Walther Neuper <neuper@ist.tugraz.at> [Fri, 27 Aug 2010 10:28:44 +0200] rev 37952
updated remaining *.ML files attached to *.thy
# '\' ---> '"' | '" ^'
# *.thy ---> (theory "*")
...THIS IS STILL MISSING FOR THE PREVIOUS *.ML
# linwidth 80
# deleted most out-commented stuff
Walther Neuper <neuper@ist.tugraz.at> [Thu, 26 Aug 2010 18:21:14 +0200] rev 37951
removed the *.ML files related to the above 8 thy's
Walther Neuper <neuper@ist.tugraz.at> [Thu, 26 Aug 2010 18:15:30 +0200] rev 37950
updated initial 8 thy's syntax without evaluation
Walther Neuper <neuper@ist.tugraz.at> [Thu, 26 Aug 2010 10:03:53 +0200] rev 37949
messed file dependencies.
The mess becomes apparent when unduly simplifying to
'theory Atools imports Complex_Main'
(*theory Atools imports Descript Typefix begin ...WOULD BE REQUIRED,
but hangs -- this needs to be clarified as well*):
The simplified header + use/s "../ProgLang/term.sml" removed:
*** Error (line 127 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Atools.thy"):
*** Value or constructor (vars) has not been declared
but now arrive at:
*** Error (line 26 of "/usr/local/isabisac/src/Tools/isac/ProgLang/term.sml"):
*** Value or constructor (indent) has not been declared
which is definitely a mess, because ProgLang/term.sml appeared
already earlier in Build_Isac.thy
Walther Neuper <neuper@ist.tugraz.at> [Wed, 25 Aug 2010 16:49:56 +0200] rev 37948
stuck at Atools.thy again; resume test on dependencies
Walther Neuper <neuper@ist.tugraz.at> [Wed, 25 Aug 2010 16:20:07 +0200] rev 37947
renamed isac's directories and Build_Isac.thy
Scripts --> ProgLang
ME --> Interpret
IsacKnowledge --> Knowledge
Walther Neuper <neuper@ist.tugraz.at> [Wed, 25 Aug 2010 15:15:01 +0200] rev 37946
dependencies of isac files clarified in test
"a --- b" means "b is dependent on a":
(dependencies between *.sml are not made explicit by Isabelle)
# library.sml, calcelems.sml, Scripts/term_G.sml --- Script.thy (see ListG.thy)
# Script.thy --- Scripts/scrtools.sml
# library.sml, calcelems.sml, Scripts/*.sml --- ME
# ME --- xmlsrc
# xmlsrc --- FE-interface
# Script.thy --- IsacKnowledge/*.thy (see IsacKnowledge/*.thy)
Walther Neuper <neuper@ist.tugraz.at> [Tue, 24 Aug 2010 12:18:27 +0200] rev 37945
trial on organizing dependencies, not successful
Typefix.thy and Descript.thy evaluated without error,
step in Isacv_Mthengine.thy to use_thy"IsakKnowledge/Atools" hangs
Walther Neuper <neuper@ist.tugraz.at> [Tue, 24 Aug 2010 11:46:09 +0200] rev 37944
start of (re-?)organizing dependencies between isac's files
Current Error:
*** Theory loader: unresolved dependencies of theory "Typefix" on file(s):
"../Scripts/scrtools.sml", "../ME/mstools.sml", "../ME/ctree.sml", ....
*** At command "end" (line 43 of "/usr/local/isabisac/src/Tools/isac/IsacKnowledge/Typefix.thy")
Walther Neuper <neuper@ist.tugraz.at> [Mon, 23 Aug 2010 17:10:57 +0200] rev 37943
updated Typefis.thy, removed Float*, Complex* (already in Isabelle2009-2)
only thy-dependency to be updated in Atools.thy