PIDE: last step of libisabelle/doc/test--isac-java--isac-kernel.txt
authorWalther Neuper <wneuper@ist.tugraz.at>
Sat, 30 May 2015 10:13:04 +0200
changeset 59130a057c00dbb94
parent 59129 b5770c988153
child 59131 ebe72566bf00
PIDE: last step of libisabelle/doc/test--isac-java--isac-kernel.txt

at https://github.com/wneuper/libisabelle/
src/Tools/isac/Frontend/interface.sml
src/Tools/isac/xmlsrc/interface-xml.sml
     1.1 --- a/src/Tools/isac/Frontend/interface.sml	Sat May 30 10:02:49 2015 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Sat May 30 10:13:04 2015 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  signature INTERFACE =
     1.5    sig
     1.6      val CalcTree : fmz list -> XML.tree
     1.7 -    val DEconstrCalcTree : calcID -> unit
     1.8 +    val DEconstrCalcTree : calcID -> XML.tree
     1.9      val Iterator : calcID -> XML.tree
    1.10      val IteratorTEST : calcID -> iterID
    1.11      val appendFormula : calcID -> cterm' -> unit (*future*)
     2.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml	Sat May 30 10:02:49 2015 +0200
     2.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml	Sat May 30 10:13:04 2015 +0200
     2.3 @@ -56,6 +56,9 @@
     2.4  	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
     2.5  	     "</DELCALC>\n" ^
     2.6  	     "@@@@@end@@@@@");
     2.7 +fun deconstructcalctreeOK2xml (calcid : calcID) = 
     2.8 +  XML.Elem (("DELCALC", []),
     2.9 +    [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])    
    2.10  
    2.11  fun iteratorOK2xml (cI:calcID) (p:pos')= 
    2.12      writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^