1.1 --- a/src/sml/ROOT.ML Sat Sep 30 11:39:40 2006 +0200
1.2 +++ b/src/sml/ROOT.ML Tue Oct 03 16:53:46 2006 +0200
1.3 @@ -187,46 +187,24 @@
1.4 use"ROOT.ML";
1.5
1.6 *****************************************************************************
1.7 -WN.notebook: create HTML representation for theory files für Isac
1.8 +WN.notebook: create HTML representation for theory files für Isac
1.9 -----------------------------------------------------------------------------
1.10 - su
1.11 - cd /home/neuper/develop
1.12 - mv sml Isac
1.13 ------
1.14 - /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/develop/Isac/
1.15 - (*^^^ does not create a new heap !!!*)
1.16 -
1.17 -^^^ old ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1.18 -WN060917vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvlead to ERROR vvvvvvvvvvv
1.19 +su
1.20 cd /home/neuper/proto2/isac/src/
1.21 mv sml Isac
1.22 +mv Isac/ROOT.ML Isac/ROOT.ML-save
1.23 +cp Isac/RCODE-root.sml Isac/ROOT.ML
1.24 +(*!!!cd"sml";!!! in ROOT.ML-save causes SysErr ("chdir failed", SOME ENOENT)*)
1.25
1.26 /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/proto2/isac/src/Isac/
1.27 -(*^^^ does not create a new heap !!!*)
1.28 +(*^^^ does not create a new heap and writes only NEW files ...
1.29 + ... to isab-installation vvv*)
1.30 +cd /usr/local/Isabelle2002/browser_info/HOL/HOL-Real/
1.31 +cp -r Isac/ ~/proto2/www/kbase/thy/browser_info/HOL/HOL-Real/
1.32
1.33 mv Isac sml
1.34 -
1.35 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ERROR~~~~~~~~~~~~
1.36 -ERROR.WN060917: !!!!! mv Isac sml DONE !!!!!
1.37 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ERROR~~~~~~~~~~~~
1.38 -neuper:/home/neuper/proto2/isac/src# /usr/local/Isabelle2002/bin/isatool usedir -i true HOL-Real /home/neuper/proto2/isac/src/Isac/
1.39 -Running HOL-Real-Isac ...
1.40 -HOL-Real-Isac FAILED
1.41 -(see also /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/log/HOL-Real-Isac)
1.42 -
1.43 - (Free ("y", "RealDef.real => RealDef.real") $ ...) $
1.44 - (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.45 - ...) : Term.term
1.46 -val it = "----- functions comming from:" : string
1.47 -### Theory loader: undeclared dependency of theory "Isac" on file: "biegelinie.sml"
1.48 -val it = () : unit
1.49 -val it = () : unit
1.50 -val it = "**** run tests on IsacKnowledge complete ****************" : string
1.51 -Exception- SysErr ("chdir failed", SOME ENOENT) raised
1.52 -SysErr ("chdir failed", SOME ENOENT)
1.53 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ERROR~~~~~~~~~~~~
1.54 -
1.55 -
1.56 +mv sml/ROOT.ML-save sml/ROOT.ML
1.57 +exit
1.58
1.59 *****************************************************************************
1.60 export of problems and methods from sml to xml