1.1 --- a/src/sml/ROOT.ML	Sun Sep 17 00:32:14 2006 +0200
     1.2 +++ b/src/sml/ROOT.ML	Mon Sep 25 16:55:17 2006 +0200
     1.3 @@ -196,6 +196,38 @@
     1.4    /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/develop/Isac/
     1.5    (*^^^ does not create a new heap !!!*)
     1.6  
     1.7 +^^^ old ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     1.8 +WN060917vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvlead to ERROR vvvvvvvvvvv
     1.9 +cd /home/neuper/proto2/isac/src/
    1.10 +mv sml Isac
    1.11 +
    1.12 +/usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/proto2/isac/src/Isac/
    1.13 +(*^^^ does not create a new heap !!!*)
    1.14 +
    1.15 +mv Isac sml
    1.16 +
    1.17 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ERROR~~~~~~~~~~~~
    1.18 +ERROR.WN060917: !!!!! mv Isac sml DONE !!!!!
    1.19 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ERROR~~~~~~~~~~~~
    1.20 +neuper:/home/neuper/proto2/isac/src# /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/proto2/isac/src/Isac/
    1.21 +Running HOL-Real-Isac ...
    1.22 +HOL-Real-Isac FAILED
    1.23 +(see also /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/log/HOL-Real-Isac)
    1.24 +
    1.25 +         (Free ("y", "RealDef.real => RealDef.real") $ ...) $
    1.26 +      (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
    1.27 +         ...) : Term.term
    1.28 +val it = "----- functions comming from:" : string
    1.29 +### Theory loader: undeclared dependency of theory "Isac" on file: "biegelinie.sml"
    1.30 +val it = () : unit
    1.31 +val it = () : unit
    1.32 +val it = "**** run tests on IsacKnowledge complete ****************" : string
    1.33 +Exception- SysErr ("chdir failed", SOME ENOENT) raised
    1.34 +SysErr ("chdir failed", SOME ENOENT)
    1.35 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ERROR~~~~~~~~~~~~
    1.36 +
    1.37 +
    1.38 +
    1.39  *****************************************************************************
    1.40  export of problems and methods from sml to xml
    1.41  -----------------------------------------------------------------------------

     2.1 --- a/src/sml/xmlsrc/thy-hierarchy.sml	Sun Sep 17 00:32:14 2006 +0200
     2.2 +++ b/src/sml/xmlsrc/thy-hierarchy.sml	Mon Sep 25 16:55:17 2006 +0200
     2.3 @@ -214,8 +214,7 @@
     2.4      "<HTMLDATA>\n" ^
     2.5      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
     2.6      id2xml i theID ^
     2.7 -    indt i ^ "<EXPLANATIONS>" ^ html ^ "\n" ^
     2.8 -    indt i ^ "</EXPLANATIONS>\n" ^
     2.9 +    indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
    2.10      authors2xml i "MATHAUTHORS" mathauthors ^
    2.11      authors2xml i "COURSEDESIGNS" coursedesign ^
    2.12      "</HTMLDATA>\n" : xml
    2.13 @@ -230,7 +229,7 @@
    2.14  		\kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
    2.15  		nth 2 theID ^ ".html") ^
    2.16      indt i ^  "</PROOF>\n" ^
    2.17 -    indt i ^ "<EXPLANATIONS>   </EXPLANATIONS>\n" ^
    2.18 +    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
    2.19      authors2xml i "MATHAUTHORS" mathauthors ^
    2.20      authors2xml i "COURSEDESIGNS" coursedesign ^
    2.21      "</THEOREMDATA>\n"
    2.22 @@ -242,7 +241,7 @@
    2.23      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
    2.24      id2xml i theID ^
    2.25      rls2xml i thy_rls ^
    2.26 -    indt i ^ "<EXPLANATIONS>   </EXPLANATIONS>\n" ^
    2.27 +    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
    2.28      authors2xml i "MATHAUTHORS" mathauthors ^
    2.29      authors2xml i "COURSEDESIGNS" coursedesign ^
    2.30      "</RULESETDATA>\n"
    2.31 @@ -254,7 +253,7 @@
    2.32      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
    2.33      id2xml i theID ^
    2.34      calc2xml i (theID2thyID theID, calc) ^
    2.35 -    indt i ^ "<EXPLANATIONS>   </EXPLANATIONS>\n" ^
    2.36 +    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
    2.37      authors2xml i "MATHAUTHORS" mathauthors ^
    2.38      authors2xml i "COURSEDESIGNS" coursedesign ^
    2.39      "</RULESETDATA>\n"