1.1 --- a/src/Tools/isac/Isac_Mathengine.thy Mon Aug 23 11:05:54 2010 +0200
1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Mon Aug 23 11:12:59 2010 +0200
1.3 @@ -48,29 +48,21 @@
1.4 use "xmlsrc/datatypes.sml"
1.5 use "xmlsrc/pbl-met-hierarchy.sml"
1.6 use "xmlsrc/thy-hierarchy.sml"
1.7 +use "xmlsrc/interface-xml.sml"
1.8 +
1.9
1.10 ML {*
1.11 @{theory "Script"};
1.12 (theory "Script");
1.13 *}
1.14
1.15 -use "xmlsrc/interface-xml.sml"
1.16 +use "FE-interface/messages.sml"
1.17
1.18 -ML {*
1.19 -Thm.get_name_hint @{thm refl};
1.20 -Thm.get_kind @{thm refl};
1.21 -*}
1.22
1.23
1.24
1.25
1.26 ML {*
1.27 -Thm.derivation_name @{thm sym};
1.28 -subtract op = [1,2,3] [3,4,5];
1.29 -*}
1.30 -
1.31 -
1.32 -ML {*
1.33 val thy = @{theory "Script"};
1.34
1.35 *}
1.36 @@ -78,7 +70,6 @@
1.37 (*
1.38
1.39
1.40 -use "FE-interface/messages.sml"
1.41 use "FE-interface/states.sml"
1.42 use "FE-interface/interface.sml"
1.43
2.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Mon Aug 23 11:05:54 2010 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Mon Aug 23 11:12:59 2010 +0200
2.3 @@ -25,154 +25,154 @@
2.4 (** add and delete users -----------------------------------------------
2.5 FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)
2.6 fun adduserOK2xml (cI:calcID) (uI:iterID) =
2.7 - writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\
2.8 - \<ADDUSER>\n\
2.9 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.10 - \ <USERID> "^string_of_int uI^" </USERID>\n\
2.11 - \</ADDUSER>\n\
2.12 - \@@@@@end@@@@@");
2.13 + writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
2.14 + "<ADDUSER>\n" ^
2.15 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.16 + " <USERID> "^string_of_int uI^" </USERID>\n" ^
2.17 + "</ADDUSER>\n" ^
2.18 + "@@@@@end@@@@@");
2.19 fun deluserOK2xml (cI:calcID) (uI:iterID) =
2.20 - writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\
2.21 - \<DELUSER>\n\
2.22 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.23 - \ <USERID> "^string_of_int uI^" </USERID>\n\
2.24 - \</DELUSER>\n\
2.25 - \@@@@@end@@@@@");
2.26 + writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
2.27 + "<DELUSER>\n" ^
2.28 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.29 + " <USERID> "^string_of_int uI^" </USERID>\n" ^
2.30 + "</DELUSER>\n" ^
2.31 + "@@@@@end@@@@@");
2.32 (*---------------------------------------------------------------------*)
2.33
2.34 fun calctreeOK2xml (*uI:iterID*) (cI:calcID) =
2.35 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.36 - \<CALCTREE>\n\
2.37 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.38 - \</CALCTREE>\n\
2.39 - \@@@@@end@@@@@");
2.40 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.41 + "<CALCTREE>\n" ^
2.42 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.43 + "</CALCTREE>\n" ^
2.44 + "@@@@@end@@@@@");
2.45 fun deconstructcalctreeOK2xml (*uI:userID*) (cI:calcID) =
2.46 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.47 - \<DELCALC>\n\
2.48 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.49 - \</DELCALC>\n\
2.50 - \@@@@@end@@@@@");
2.51 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.52 + "<DELCALC>\n" ^
2.53 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.54 + "</DELCALC>\n" ^
2.55 + "@@@@@end@@@@@");
2.56
2.57 fun iteratorOK2xml (cI:calcID) (p:pos')=
2.58 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.59 - \<CALCITERATOR>\n\
2.60 - \ <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.61 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.62 + "<CALCITERATOR>\n" ^
2.63 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.64 pos'2xml i ("POSITION", p) ^
2.65 - "</CALCITERATOR>\n\
2.66 - \@@@@@end@@@@@");
2.67 + "</CALCITERATOR>\n" ^
2.68 + "@@@@@end@@@@@");
2.69 fun iteratorERROR2xml (cI:calcID) =
2.70 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.71 - \<CALCITERATOR>\n\
2.72 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.73 - \ <ERROR> pos does not exist </ERROR>\n\
2.74 - \</CALCITERATOR>\n\
2.75 - \@@@@@end@@@@@");
2.76 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.77 + "<CALCITERATOR>\n" ^
2.78 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.79 + " <ERROR> pos does not exist </ERROR>\n" ^
2.80 + "</CALCITERATOR>\n" ^
2.81 + "@@@@@end@@@@@");
2.82
2.83 fun sysERROR2xml (cI:calcID) "" =
2.84 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.85 - \<SYSERROR>\n\
2.86 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.87 - \ <ERROR> in kernel </ERROR>\n\
2.88 - \</SYSERROR>\n\
2.89 - \@@@@@end@@@@@")
2.90 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.91 + "<SYSERROR>\n" ^
2.92 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.93 + " <ERROR> in kernel </ERROR>\n" ^
2.94 + "</SYSERROR>\n" ^
2.95 + "@@@@@end@@@@@")
2.96 | sysERROR2xml (cI:calcID) str =
2.97 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.98 - \<SYSERROR>\n\
2.99 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.100 - \ <ERROR> "^str^" </ERROR>\n\
2.101 - \</SYSERROR>\n\
2.102 - \@@@@@end@@@@@");
2.103 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.104 + "<SYSERROR>\n" ^
2.105 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.106 + " <ERROR> "^str^" </ERROR>\n" ^
2.107 + "</SYSERROR>\n" ^
2.108 + "@@@@@end@@@@@");
2.109
2.110 fun refformulaOK2xml (cI:calcID) p (Form t) =
2.111 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.112 - \<REFFORMULA>\n\
2.113 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.114 - \ <CALCFORMULA>\n"^
2.115 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.116 + "<REFFORMULA>\n" ^
2.117 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.118 + " <CALCFORMULA>\n"^
2.119 pos'2xml (2*i) ("POSITION", p) ^
2.120 - " <FORMULA>"^
2.121 - term2xml (2*i) t ^"\n"^
2.122 - " </FORMULA>\n\
2.123 - \ </CALCFORMULA>\n\
2.124 - \</REFFORMULA>\n\
2.125 - \@@@@@end@@@@@")
2.126 + " <FORMULA>" ^
2.127 + term2xml (2*i) t ^ "\n" ^
2.128 + " </FORMULA>\n" ^
2.129 + " </CALCFORMULA>\n" ^
2.130 + "</REFFORMULA>\n" ^
2.131 + "@@@@@end@@@@@")
2.132 | refformulaOK2xml (cI:calcID) p (ModSpec modspec) =
2.133 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.134 - \<REFFORMULA>\n\
2.135 - \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
2.136 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.137 + "<REFFORMULA>\n" ^
2.138 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.139 pos'calchead2xml i (p, modspec)^
2.140 - "</REFFORMULA>\n\
2.141 - \@@@@@end@@@@@");
2.142 + "</REFFORMULA>\n" ^
2.143 + "@@@@@end@@@@@");
2.144
2.145 fun refformulaERROR2xml (cI:calcID) = (*FIXME.WN.29.8.03 unused*)
2.146 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.147 - \<REFFORMULA>\n\
2.148 - \ <ERROR> object is not a formula </ERROR>\n\
2.149 - \</REFFORMULA>\n\
2.150 - \@@@@@end@@@@@");
2.151 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.152 + "<REFFORMULA>\n" ^
2.153 + " <ERROR> object is not a formula </ERROR>\n" ^
2.154 + "</REFFORMULA>\n" ^
2.155 + "@@@@@end@@@@@");
2.156
2.157 (* val (cI, tac) = (cI, ta);
2.158 *)
2.159 fun gettacticOK2xml (cI:calcID) tac =
2.160 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.161 - \<GETTACTIC>\n\
2.162 - \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
2.163 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.164 + "<GETTACTIC>\n" ^
2.165 + " <CALCID> "^string_of_int cI^" </CALCID>\n"^
2.166 tac2xml i tac^
2.167 - "</GETTACTIC>\n\
2.168 - \@@@@@end@@@@@");
2.169 + "</GETTACTIC>\n" ^
2.170 + "@@@@@end@@@@@");
2.171 fun gettacticERROR2xml (cI:calcID) str =
2.172 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.173 - \<GETTACTIC>\n\
2.174 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.175 - \ <ERROR> "^str^" </ERROR>\n\
2.176 - \</GETTACTIC>\n\
2.177 - \@@@@@end@@@@@");
2.178 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.179 + "<GETTACTIC>\n" ^
2.180 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.181 + " <ERROR> "^str^" </ERROR>\n" ^
2.182 + "</GETTACTIC>\n" ^
2.183 + "@@@@@end@@@@@");
2.184
2.185 fun applicabletacticsOK cI tacs =
2.186 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.187 - \<APPLICABLETACTICS>\n\
2.188 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.189 - \ <TACLIST>\n"^
2.190 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.191 + "<APPLICABLETACTICS>\n" ^
2.192 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.193 + " <TACLIST>\n"^
2.194 tacs2xml (2*i) tacs^
2.195 - " </TACLIST>\n\
2.196 - \</APPLICABLETACTICS>\n\
2.197 - \@@@@@end@@@@@");
2.198 + " </TACLIST>\n" ^
2.199 + "</APPLICABLETACTICS>\n" ^
2.200 + "@@@@@end@@@@@");
2.201
2.202 fun getasmsOK2xml (cI:calcID) terms =
2.203 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.204 - \<GETASSUMPTIONS>\n\
2.205 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.206 - \ <ASMLIST>\n"^
2.207 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.208 + "<GETASSUMPTIONS>\n" ^
2.209 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.210 + " <ASMLIST>\n"^
2.211 formulae2xml (i+i) terms ^
2.212 - " </ASMLIST>\n\
2.213 - \</GETASSUMPTIONS>\n\
2.214 - \@@@@@end@@@@@");
2.215 + " </ASMLIST>\n" ^
2.216 + "</GETASSUMPTIONS>\n" ^
2.217 + "@@@@@end@@@@@");
2.218 (* getasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
2.219 *)
2.220
2.221 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
2.222 fun getaccuasmsOK2xml cI asms =
2.223 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.224 - \<GETACCUMULATEDASMS>\n\
2.225 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.226 - \ <ASMLIST>\n"^
2.227 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.228 + "<GETACCUMULATEDASMS>\n" ^
2.229 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.230 + " <ASMLIST>\n"^
2.231 formulae2xml (i+i) asms^
2.232 - " </ASMLIST>\n\
2.233 - \</GETACCUMULATEDASMS>\n\
2.234 - \@@@@@end@@@@@");
2.235 + " </ASMLIST>\n" ^
2.236 + "</GETACCUMULATEDASMS>\n" ^
2.237 + "@@@@@end@@@@@");
2.238 (* getaccuasmsOK2xml 333 [(([1],Res), str2term "1+1=2"),
2.239 (([2],Res), str2term "1+1+1=3")];
2.240 getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
2.241 *)
2.242
2.243 fun getintervalOK (cI:calcID) fs =
2.244 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.245 - \<GETELEMENTSFROMTO>\n\
2.246 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.247 - \ <FORMHEADS>\n"^
2.248 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.249 + "<GETELEMENTSFROMTO>\n" ^
2.250 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.251 + " <FORMHEADS>\n"^
2.252 posterms2xml (2*i) fs^
2.253 - " </FORMHEADS>\n\
2.254 - \</GETELEMENTSFROMTO>\n\
2.255 - \@@@@@end@@@@@");
2.256 + " </FORMHEADS>\n" ^
2.257 + "</GETELEMENTSFROMTO>\n" ^
2.258 + "@@@@@end@@@@@");
2.259
2.260
2.261 fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =
2.262 @@ -186,8 +186,8 @@
2.263 term2xml i hdl ^ "\n" ^
2.264 " </HEAD>\n" ^
2.265 model2xml i pbl pre ^
2.266 - "</CONTEXTPBL>\n\
2.267 - \@@@@@end@@@@@");
2.268 + "</CONTEXTPBL>\n" ^
2.269 + "@@@@@end@@@@@");
2.270
2.271 fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =
2.272 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.273 @@ -198,145 +198,145 @@
2.274 else "incorrect") ^ " </STATUS>\n" ^
2.275 scr2xml i scr ^
2.276 model2xml i pbl pre ^
2.277 - "</CONTEXTMET>\n\
2.278 - \@@@@@end@@@@@");
2.279 + "</CONTEXTMET>\n" ^
2.280 + "@@@@@end@@@@@");
2.281
2.282
2.283 fun tryrefineOK2xml (cI:calcID) (ModSpec modspec) =
2.284 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.285 - \<TRYREFINE>\n\
2.286 - \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
2.287 - modspec2xml i modspec^
2.288 - "</TRYREFINE>\n\
2.289 - \@@@@@end@@@@@");
2.290 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.291 + "<TRYREFINE>\n" ^
2.292 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.293 + modspec2xml i modspec ^
2.294 + "</TRYREFINE>\n" ^
2.295 + "@@@@@end@@@@@");
2.296
2.297 fun appendformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
2.298 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.299 - \<APPENDFORMULA>\n\
2.300 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.301 - \ <CALCCHANGED>\n" ^
2.302 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.303 + "<APPENDFORMULA>\n" ^
2.304 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.305 + " <CALCCHANGED>\n" ^
2.306 pos'2xml (2*i) ("UNCHANGED", old) ^
2.307 pos'2xml (2*i) ("DELETED", del) ^
2.308 pos'2xml (2*i) ("GENERATED", new) ^
2.309 - " </CALCCHANGED>\n\
2.310 - \</APPENDFORMULA>\n\
2.311 - \@@@@@end@@@@@");
2.312 + " </CALCCHANGED>\n" ^
2.313 + "</APPENDFORMULA>\n" ^
2.314 + "@@@@@end@@@@@");
2.315 (* appendformulaOK2xml 1 ([2],Frm) ([3],Pbl) ([4],Res);
2.316 *)
2.317 fun appendformulaERROR2xml (cI:calcID) msg =
2.318 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.319 - \<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n\
2.320 - \@@@@@end@@@@@");
2.321 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.322 + "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
2.323 + "@@@@@end@@@@@");
2.324
2.325 fun replaceformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
2.326 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.327 - \<REPLACEFORMULA>\n\
2.328 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.329 - \ <CALCCHANGED>\n" ^
2.330 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.331 + "<REPLACEFORMULA>\n" ^
2.332 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.333 + " <CALCCHANGED>\n" ^
2.334 pos'2xml (2*i) ("UNCHANGED", old) ^
2.335 pos'2xml (2*i) ("DELETED", del) ^
2.336 pos'2xml (2*i) ("GENERATED", new) ^
2.337 - " </CALCCHANGED>\n\
2.338 - \</REPLACEFORMULA>\n\
2.339 - \@@@@@end@@@@@");
2.340 + " </CALCCHANGED>\n" ^
2.341 + "</REPLACEFORMULA>\n" ^
2.342 + "@@@@@end@@@@@");
2.343 fun replaceformulaERROR2xml (cI:calcID) msg =
2.344 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.345 - \<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n\
2.346 - \@@@@@end@@@@@");
2.347 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.348 + "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
2.349 + "@@@@@end@@@@@");
2.350
2.351 fun message2xml (cI:calcID) e =
2.352 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.353 - \<MESSAGE>\n\
2.354 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.355 - \ <STRING> "^e^" </STRING>\n\
2.356 - \</MESSAGE>\n\
2.357 - \@@@@@end@@@@@");
2.358 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.359 + "<MESSAGE>\n" ^
2.360 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.361 + " <STRING> "^e^" </STRING>\n" ^
2.362 + "</MESSAGE>\n" ^
2.363 + "@@@@@end@@@@@");
2.364
2.365 fun setnexttactic2xml (*uI:iterID*) (cI:calcID) e =
2.366 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.367 - \<SETNEXTTACTIC>\n\
2.368 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.369 - \ <MESSAGE> "^e^" </MESSAGE>\n\
2.370 - \</SETNEXTTACTIC>\n\
2.371 - \@@@@@end@@@@@");
2.372 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.373 + "<SETNEXTTACTIC>\n" ^
2.374 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.375 + " <MESSAGE> "^e^" </MESSAGE>\n" ^
2.376 + "</SETNEXTTACTIC>\n" ^
2.377 + "@@@@@end@@@@@");
2.378
2.379 fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac =
2.380 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.381 - \<NEXTTAC>\n\
2.382 - \ <CALCID> "^string_of_int cI^" </CALCID>\n"^
2.383 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.384 + "<NEXTTAC>\n" ^
2.385 + " <CALCID> "^string_of_int cI^" </CALCID>\n"^
2.386 tac2xml i tac^
2.387 (* ^(strs2xml o (map (tac2xml i))) tacs^*)
2.388 - "</NEXTTAC>\n\
2.389 - \@@@@@end@@@@@");
2.390 + "</NEXTTAC>\n" ^
2.391 + "@@@@@end@@@@@");
2.392 (* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
2.393 *)
2.394 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e =
2.395 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.396 - \<NEXTTAC>\n\
2.397 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.398 - \ <ERROR> "^ e ^" </ERROR>\n\
2.399 - \</NEXTTAC>\n\
2.400 - \@@@@@end@@@@@");
2.401 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.402 + "<NEXTTAC>\n" ^
2.403 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.404 + " <ERROR> "^ e ^" </ERROR>\n" ^
2.405 + "</NEXTTAC>\n" ^
2.406 + "@@@@@end@@@@@");
2.407
2.408 (*. UNCHANGED: the pos' of the active formula autocalculate has been applied at
2.409 DELETED: last pos' of the succesional sequence of formulae prob. deleted
2.410 GENERATED: the pos' of the new active formula
2.411 .*)
2.412 fun autocalculateOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
2.413 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.414 - \<AUTOCALC>\n\
2.415 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.416 - \ <CALCCHANGED>\n" ^
2.417 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.418 + "<AUTOCALC>\n" ^
2.419 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.420 + " <CALCCHANGED>\n" ^
2.421 pos'2xml (2*i) ("UNCHANGED", old) ^
2.422 pos'2xml (2*i) ("DELETED", del) ^
2.423 pos'2xml (2*i) ("GENERATED", new) ^
2.424 - " </CALCCHANGED>\n\
2.425 - \</AUTOCALC>\n\
2.426 - \@@@@@end@@@@@");
2.427 + " </CALCCHANGED>\n" ^
2.428 + "</AUTOCALC>\n" ^
2.429 + "@@@@@end@@@@@");
2.430 (* autocalculate2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
2.431 *)
2.432 fun autocalculateERROR2xml (cI:calcID) e =
2.433 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.434 - \<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n\
2.435 - \@@@@@end@@@@@");
2.436 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.437 + "<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
2.438 + "@@@@@end@@@@@");
2.439
2.440 fun interStepsOK (cI:calcID) (*pos'forms*) (old:pos') (del:pos') (new:pos') =
2.441 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.442 - \<INTERSTEPS>\n\
2.443 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.444 - \ <CALCCHANGED>\n" ^
2.445 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.446 + "<INTERSTEPS>\n" ^
2.447 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.448 + " <CALCCHANGED>\n" ^
2.449 pos'2xml (2*i) ("UNCHANGED", old) ^
2.450 pos'2xml (2*i) ("DELETED", del) ^
2.451 pos'2xml (2*i) ("GENERATED", new) ^
2.452 - " </CALCCHANGED>\n\
2.453 - \</INTERSTEPS>\n\
2.454 - \@@@@@end@@@@@");
2.455 + " </CALCCHANGED>\n" ^
2.456 + "</INTERSTEPS>\n" ^
2.457 + "@@@@@end@@@@@");
2.458 fun interStepsERROR (cI:calcID) e =
2.459 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.460 - \ <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n\
2.461 - \@@@@@end@@@@@");
2.462 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.463 + " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
2.464 + "@@@@@end@@@@@");
2.465
2.466 fun modifycalcheadOK2xml (cI:calcID) (chd as (complete,p_,_,_,_,_):ocalhd) =
2.467 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.468 - \<MODIFYCALCHEAD>\n\
2.469 - \ <CALCID> "^string_of_int cI^" </CALCID>\n\
2.470 - \ <STATUS> "^(if complete then "complete"
2.471 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.472 + "<MODIFYCALCHEAD>\n" ^
2.473 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.474 + " <STATUS> "^(if complete then "complete"
2.475 else "incomplete")^ "</STATUS>\n"^
2.476 modspec2xml i chd^
2.477 - "</MODIFYCALCHEAD>\n\
2.478 - \@@@@@end@@@@@");
2.479 + "</MODIFYCALCHEAD>\n" ^
2.480 + "@@@@@end@@@@@");
2.481
2.482 (* val (cI, contthy) = (cI, (context_thy (pt,pos) tac));
2.483 *)
2.484 fun contextthyOK2xml cI contthy =
2.485 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
2.486 - \<CONTEXTTHY>\n\
2.487 - \ <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.488 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.489 + "<CONTEXTTHY>\n" ^
2.490 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.491 contthy2xml i contthy ^
2.492 - "</CONTEXTTHY>\n\
2.493 - \@@@@@end@@@@@");
2.494 + "</CONTEXTTHY>\n" ^
2.495 + "@@@@@end@@@@@");
2.496
2.497 (*
2.498 fun contextthyNO2xml guh =
2.499 writeln (datatypes.contextthyNO2xml 0 guh);
2.500 -*)
2.501 \ No newline at end of file
2.502 +*)