src/Tools/isac/xmlsrc/interface-xml.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 38015 67ba02dffacc
child 42430 5b629bb1c073
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba
    23 
    23 
    24 
    24 
    25 (** add and delete users -----------------------------------------------
    25 (** add and delete users -----------------------------------------------
    26  FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)
    26  FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)
    27 fun adduserOK2xml (cI:calcID) (uI:iterID) = 
    27 fun adduserOK2xml (cI:calcID) (uI:iterID) = 
    28     tracing ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
    28     writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
    29 	     "<ADDUSER>\n" ^
    29 	     "<ADDUSER>\n" ^
    30 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    30 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    31 	     "  <USERID> "^string_of_int uI^" </USERID>\n" ^
    31 	     "  <USERID> "^string_of_int uI^" </USERID>\n" ^
    32 	     "</ADDUSER>\n" ^
    32 	     "</ADDUSER>\n" ^
    33 	     "@@@@@end@@@@@");
    33 	     "@@@@@end@@@@@");
    34 fun deluserOK2xml (cI:calcID) (uI:iterID) = 
    34 fun deluserOK2xml (cI:calcID) (uI:iterID) = 
    35     tracing ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
    35     writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n" ^
    36 	     "<DELUSER>\n" ^
    36 	     "<DELUSER>\n" ^
    37 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    37 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    38 	     "  <USERID> "^string_of_int uI^" </USERID>\n" ^
    38 	     "  <USERID> "^string_of_int uI^" </USERID>\n" ^
    39 	     "</DELUSER>\n" ^
    39 	     "</DELUSER>\n" ^
    40 	     "@@@@@end@@@@@");
    40 	     "@@@@@end@@@@@");
    41 (*---------------------------------------------------------------------*)
    41 (*---------------------------------------------------------------------*)
    42 
    42 
    43 fun calctreeOK2xml (*uI:iterID*) (cI:calcID) = 
    43 fun calctreeOK2xml (*uI:iterID*) (cI:calcID) = 
    44     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    44     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    45 	     "<CALCTREE>\n" ^
    45 	     "<CALCTREE>\n" ^
    46 	     "   <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    46 	     "   <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    47 	     "</CALCTREE>\n" ^
    47 	     "</CALCTREE>\n" ^
    48 	     "@@@@@end@@@@@");
    48 	     "@@@@@end@@@@@");
    49 fun deconstructcalctreeOK2xml (*uI:userID*) (cI:calcID) = 
    49 fun deconstructcalctreeOK2xml (*uI:userID*) (cI:calcID) = 
    50     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    50     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    51 	     "<DELCALC>\n" ^
    51 	     "<DELCALC>\n" ^
    52 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    52 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    53 	     "</DELCALC>\n" ^
    53 	     "</DELCALC>\n" ^
    54 	     "@@@@@end@@@@@");
    54 	     "@@@@@end@@@@@");
    55 
    55 
    56 fun iteratorOK2xml (cI:calcID) (p:pos')= 
    56 fun iteratorOK2xml (cI:calcID) (p:pos')= 
    57     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    57     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    58 	     "<CALCITERATOR>\n" ^
    58 	     "<CALCITERATOR>\n" ^
    59 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    59 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    60 	     pos'2xml i ("POSITION", p) ^
    60 	     pos'2xml i ("POSITION", p) ^
    61 	     "</CALCITERATOR>\n" ^
    61 	     "</CALCITERATOR>\n" ^
    62 	     "@@@@@end@@@@@");
    62 	     "@@@@@end@@@@@");
    63 fun iteratorERROR2xml (cI:calcID) = 
    63 fun iteratorERROR2xml (cI:calcID) = 
    64     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    64     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    65 	     "<CALCITERATOR>\n" ^
    65 	     "<CALCITERATOR>\n" ^
    66 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    66 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    67 	     "  <ERROR> pos does not exist </ERROR>\n" ^
    67 	     "  <ERROR> pos does not exist </ERROR>\n" ^
    68 	     "</CALCITERATOR>\n" ^
    68 	     "</CALCITERATOR>\n" ^
    69 	     "@@@@@end@@@@@");
    69 	     "@@@@@end@@@@@");
    70 
    70 
    71 fun sysERROR2xml (cI:calcID) "" = 
    71 fun sysERROR2xml (cI:calcID) "" = 
    72     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    72     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    73 	     "<SYSERROR>\n" ^
    73 	     "<SYSERROR>\n" ^
    74 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    74 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    75 	     "  <ERROR> in kernel </ERROR>\n" ^
    75 	     "  <ERROR> in kernel </ERROR>\n" ^
    76 	     "</SYSERROR>\n" ^
    76 	     "</SYSERROR>\n" ^
    77 	     "@@@@@end@@@@@")
    77 	     "@@@@@end@@@@@")
    78   | sysERROR2xml (cI:calcID) str = 
    78   | sysERROR2xml (cI:calcID) str = 
    79     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    79     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    80 	     "<SYSERROR>\n" ^
    80 	     "<SYSERROR>\n" ^
    81 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    81 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    82 	     "  <ERROR> "^str^" </ERROR>\n" ^
    82 	     "  <ERROR> "^str^" </ERROR>\n" ^
    83 	     "</SYSERROR>\n" ^
    83 	     "</SYSERROR>\n" ^
    84 	     "@@@@@end@@@@@");
    84 	     "@@@@@end@@@@@");
    85 
    85 
    86 fun refformulaOK2xml (cI:calcID) p (Form t) = 
    86 fun refformulaOK2xml (cI:calcID) p (Form t) = 
    87     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    87     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    88 	     "<REFFORMULA>\n" ^
    88 	     "<REFFORMULA>\n" ^
    89              "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    89              "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
    90 	     "  <CALCFORMULA>\n"^
    90 	     "  <CALCFORMULA>\n"^
    91 	     pos'2xml (2*i) ("POSITION", p) ^
    91 	     pos'2xml (2*i) ("POSITION", p) ^
    92 	     "    <FORMULA>" ^
    92 	     "    <FORMULA>" ^
    94 	     "    </FORMULA>\n" ^
    94 	     "    </FORMULA>\n" ^
    95 	     "  </CALCFORMULA>\n" ^
    95 	     "  </CALCFORMULA>\n" ^
    96 	     "</REFFORMULA>\n" ^
    96 	     "</REFFORMULA>\n" ^
    97 	     "@@@@@end@@@@@") 
    97 	     "@@@@@end@@@@@") 
    98   | refformulaOK2xml (cI:calcID) p (ModSpec modspec) =
    98   | refformulaOK2xml (cI:calcID) p (ModSpec modspec) =
    99     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
    99     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   100 	     "<REFFORMULA>\n" ^
   100 	     "<REFFORMULA>\n" ^
   101              "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   101              "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   102 	     pos'calchead2xml i (p, modspec)^ 
   102 	     pos'calchead2xml i (p, modspec)^ 
   103 	     "</REFFORMULA>\n" ^
   103 	     "</REFFORMULA>\n" ^
   104 	     "@@@@@end@@@@@"); 
   104 	     "@@@@@end@@@@@"); 
   105 
   105 
   106 fun refformulaERROR2xml (cI:calcID) = (*FIXME.WN.29.8.03 unused*)
   106 fun refformulaERROR2xml (cI:calcID) = (*FIXME.WN.29.8.03 unused*)
   107     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   107     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   108 	     "<REFFORMULA>\n" ^
   108 	     "<REFFORMULA>\n" ^
   109 	     "   <ERROR> object is not a formula </ERROR>\n" ^
   109 	     "   <ERROR> object is not a formula </ERROR>\n" ^
   110 	     "</REFFORMULA>\n" ^
   110 	     "</REFFORMULA>\n" ^
   111 	     "@@@@@end@@@@@");
   111 	     "@@@@@end@@@@@");
   112 
   112 
   113 (* val (cI, tac) = (cI, ta);
   113 (* val (cI, tac) = (cI, ta);
   114    *)
   114    *)
   115 fun gettacticOK2xml (cI:calcID) tac = 
   115 fun gettacticOK2xml (cI:calcID) tac = 
   116     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   116     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   117 	     "<GETTACTIC>\n" ^
   117 	     "<GETTACTIC>\n" ^
   118 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n"^
   118 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n"^
   119 	     tac2xml i tac^
   119 	     tac2xml i tac^
   120 	     "</GETTACTIC>\n" ^
   120 	     "</GETTACTIC>\n" ^
   121 	     "@@@@@end@@@@@");
   121 	     "@@@@@end@@@@@");
   122 fun gettacticERROR2xml (cI:calcID) str = 
   122 fun gettacticERROR2xml (cI:calcID) str = 
   123     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   123     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   124 	     "<GETTACTIC>\n" ^
   124 	     "<GETTACTIC>\n" ^
   125 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   125 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   126 	     "  <ERROR> "^str^" </ERROR>\n" ^
   126 	     "  <ERROR> "^str^" </ERROR>\n" ^
   127 	     "</GETTACTIC>\n" ^
   127 	     "</GETTACTIC>\n" ^
   128 	     "@@@@@end@@@@@");
   128 	     "@@@@@end@@@@@");
   129 
   129 
   130 fun applicabletacticsOK cI tacs =
   130 fun applicabletacticsOK cI tacs =
   131     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   131     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   132 	     "<APPLICABLETACTICS>\n" ^
   132 	     "<APPLICABLETACTICS>\n" ^
   133 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   133 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   134 	     "  <TACLIST>\n"^
   134 	     "  <TACLIST>\n"^
   135 	     tacs2xml (2*i) tacs^
   135 	     tacs2xml (2*i) tacs^
   136 	     "  </TACLIST>\n" ^
   136 	     "  </TACLIST>\n" ^
   137 	     "</APPLICABLETACTICS>\n" ^
   137 	     "</APPLICABLETACTICS>\n" ^
   138 	     "@@@@@end@@@@@");
   138 	     "@@@@@end@@@@@");
   139 
   139 
   140 fun getasmsOK2xml (cI:calcID) terms = 
   140 fun getasmsOK2xml (cI:calcID) terms = 
   141     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   141     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   142 	     "<GETASSUMPTIONS>\n" ^
   142 	     "<GETASSUMPTIONS>\n" ^
   143 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   143 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   144 	     "  <ASMLIST>\n"^
   144 	     "  <ASMLIST>\n"^
   145 	     formulae2xml (i+i) terms ^
   145 	     formulae2xml (i+i) terms ^
   146 	     "  </ASMLIST>\n" ^
   146 	     "  </ASMLIST>\n" ^
   149 (* getasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
   149 (* getasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
   150    *)
   150    *)
   151 
   151 
   152 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
   152 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
   153 fun getaccuasmsOK2xml cI asms =
   153 fun getaccuasmsOK2xml cI asms =
   154     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   154     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   155 	     "<GETACCUMULATEDASMS>\n" ^
   155 	     "<GETACCUMULATEDASMS>\n" ^
   156 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   156 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   157 	     "  <ASMLIST>\n"^
   157 	     "  <ASMLIST>\n"^
   158 	     formulae2xml (i+i) asms^
   158 	     formulae2xml (i+i) asms^
   159 	     "  </ASMLIST>\n" ^
   159 	     "  </ASMLIST>\n" ^
   163 			  (([2],Res), str2term "1+1+1=3")];
   163 			  (([2],Res), str2term "1+1+1=3")];
   164    getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
   164    getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
   165    *)
   165    *)
   166 
   166 
   167 fun getintervalOK (cI:calcID) fs = 
   167 fun getintervalOK (cI:calcID) fs = 
   168     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   168     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   169 	     "<GETELEMENTSFROMTO>\n" ^
   169 	     "<GETELEMENTSFROMTO>\n" ^
   170 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   170 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   171 	     "  <FORMHEADS>\n"^	     
   171 	     "  <FORMHEADS>\n"^	     
   172 	     posterms2xml (2*i) fs^
   172 	     posterms2xml (2*i) fs^
   173 	     "  </FORMHEADS>\n" ^	     
   173 	     "  </FORMHEADS>\n" ^	     
   174 	     "</GETELEMENTSFROMTO>\n" ^
   174 	     "</GETELEMENTSFROMTO>\n" ^
   175 	     "@@@@@end@@@@@");
   175 	     "@@@@@end@@@@@");
   176 
   176 
   177 
   177 
   178 fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =
   178 fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =
   179     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   179     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   180 	     "<CONTEXTPBL>\n" ^
   180 	     "<CONTEXTPBL>\n" ^
   181 	     "  <GUH> " ^ pblID2guh pI ^ " </GUH>\n" ^
   181 	     "  <GUH> " ^ pblID2guh pI ^ " </GUH>\n" ^
   182 	     "  <STATUS> " ^ (if model_ok 
   182 	     "  <STATUS> " ^ (if model_ok 
   183 			     then "correct" 
   183 			     then "correct" 
   184 			     else "incorrect") ^ " </STATUS>\n" ^
   184 			     else "incorrect") ^ " </STATUS>\n" ^
   188 	     model2xml i pbl pre ^
   188 	     model2xml i pbl pre ^
   189 	     "</CONTEXTPBL>\n" ^
   189 	     "</CONTEXTPBL>\n" ^
   190 	     "@@@@@end@@@@@");
   190 	     "@@@@@end@@@@@");
   191 
   191 
   192 fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =
   192 fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =
   193     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   193     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   194 	     "<CONTEXTMET>\n" ^
   194 	     "<CONTEXTMET>\n" ^
   195 	     "  <GUH> " ^ metID2guh pI ^ " </GUH>\n" ^
   195 	     "  <GUH> " ^ metID2guh pI ^ " </GUH>\n" ^
   196 	     "  <STATUS> " ^ (if model_ok 
   196 	     "  <STATUS> " ^ (if model_ok 
   197 			     then "correct" 
   197 			     then "correct" 
   198 			     else "incorrect") ^ " </STATUS>\n" ^
   198 			     else "incorrect") ^ " </STATUS>\n" ^
   201 	     "</CONTEXTMET>\n" ^
   201 	     "</CONTEXTMET>\n" ^
   202 	     "@@@@@end@@@@@");
   202 	     "@@@@@end@@@@@");
   203 
   203 
   204 
   204 
   205 fun tryrefineOK2xml (cI:calcID) (ModSpec modspec) =
   205 fun tryrefineOK2xml (cI:calcID) (ModSpec modspec) =
   206     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   206     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   207 	     "<TRYREFINE>\n" ^
   207 	     "<TRYREFINE>\n" ^
   208              "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   208              "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   209 	     modspec2xml i modspec ^
   209 	     modspec2xml i modspec ^
   210 	     "</TRYREFINE>\n" ^
   210 	     "</TRYREFINE>\n" ^
   211 	     "@@@@@end@@@@@"); 
   211 	     "@@@@@end@@@@@"); 
   212 
   212 
   213 fun appendformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
   213 fun appendformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
   214     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   214     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   215 	     "<APPENDFORMULA>\n" ^
   215 	     "<APPENDFORMULA>\n" ^
   216 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   216 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   217 	     "  <CALCCHANGED>\n" ^
   217 	     "  <CALCCHANGED>\n" ^
   218 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   218 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   219 	     pos'2xml (2*i) ("DELETED", del) ^ 
   219 	     pos'2xml (2*i) ("DELETED", del) ^ 
   222 	     "</APPENDFORMULA>\n" ^
   222 	     "</APPENDFORMULA>\n" ^
   223 	     "@@@@@end@@@@@");
   223 	     "@@@@@end@@@@@");
   224 (* appendformulaOK2xml 1 ([2],Frm) ([3],Pbl) ([4],Res);
   224 (* appendformulaOK2xml 1 ([2],Frm) ([3],Pbl) ([4],Res);
   225    *)
   225    *)
   226 fun appendformulaERROR2xml (cI:calcID) msg =
   226 fun appendformulaERROR2xml (cI:calcID) msg =
   227     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   227     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   228 	     "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
   228 	     "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
   229 	     "@@@@@end@@@@@");
   229 	     "@@@@@end@@@@@");
   230 
   230 
   231 fun replaceformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
   231 fun replaceformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =
   232     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   232     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   233 	     "<REPLACEFORMULA>\n" ^
   233 	     "<REPLACEFORMULA>\n" ^
   234 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   234 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   235 	     "  <CALCCHANGED>\n" ^
   235 	     "  <CALCCHANGED>\n" ^
   236 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   236 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   237 	     pos'2xml (2*i) ("DELETED", del) ^ 
   237 	     pos'2xml (2*i) ("DELETED", del) ^ 
   238 	     pos'2xml (2*i) ("GENERATED", new) ^ 
   238 	     pos'2xml (2*i) ("GENERATED", new) ^ 
   239 	     "  </CALCCHANGED>\n" ^
   239 	     "  </CALCCHANGED>\n" ^
   240 	     "</REPLACEFORMULA>\n" ^
   240 	     "</REPLACEFORMULA>\n" ^
   241 	     "@@@@@end@@@@@");
   241 	     "@@@@@end@@@@@");
   242 fun replaceformulaERROR2xml (cI:calcID) msg =
   242 fun replaceformulaERROR2xml (cI:calcID) msg =
   243     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   243     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   244 	     "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
   244 	     "<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n" ^
   245 	     "@@@@@end@@@@@");
   245 	     "@@@@@end@@@@@");
   246 
   246 
   247 fun message2xml (cI:calcID) e = 
   247 fun message2xml (cI:calcID) e = 
   248     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   248     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   249 	     "<MESSAGE>\n" ^
   249 	     "<MESSAGE>\n" ^
   250 	     "   <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   250 	     "   <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   251 	     "   <STRING> "^e^" </STRING>\n" ^
   251 	     "   <STRING> "^e^" </STRING>\n" ^
   252 	     "</MESSAGE>\n" ^
   252 	     "</MESSAGE>\n" ^
   253 	     "@@@@@end@@@@@");
   253 	     "@@@@@end@@@@@");
   254 
   254 
   255 fun setnexttactic2xml (*uI:iterID*) (cI:calcID) e = 
   255 fun setnexttactic2xml (*uI:iterID*) (cI:calcID) e = 
   256     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   256     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   257 	     "<SETNEXTTACTIC>\n" ^
   257 	     "<SETNEXTTACTIC>\n" ^
   258 	     "   <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   258 	     "   <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   259 	     "   <MESSAGE> "^e^" </MESSAGE>\n" ^
   259 	     "   <MESSAGE> "^e^" </MESSAGE>\n" ^
   260 	     "</SETNEXTTACTIC>\n" ^
   260 	     "</SETNEXTTACTIC>\n" ^
   261 	     "@@@@@end@@@@@");
   261 	     "@@@@@end@@@@@");
   262 
   262 
   263 fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac = 
   263 fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac = 
   264     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   264     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   265 	     "<NEXTTAC>\n" ^
   265 	     "<NEXTTAC>\n" ^
   266 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n"^
   266 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n"^
   267 	     tac2xml i tac^
   267 	     tac2xml i tac^
   268 (*	     ^(strs2xml o (map (tac2xml i))) tacs^*)
   268 (*	     ^(strs2xml o (map (tac2xml i))) tacs^*)
   269 	     "</NEXTTAC>\n" ^
   269 	     "</NEXTTAC>\n" ^
   270 	     "@@@@@end@@@@@");
   270 	     "@@@@@end@@@@@");
   271 (* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
   271 (* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
   272    *)
   272    *)
   273 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e = 
   273 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e = 
   274     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   274     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   275 	     "<NEXTTAC>\n" ^
   275 	     "<NEXTTAC>\n" ^
   276 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   276 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   277 	     "  <ERROR> "^ e ^" </ERROR>\n" ^
   277 	     "  <ERROR> "^ e ^" </ERROR>\n" ^
   278 	     "</NEXTTAC>\n" ^
   278 	     "</NEXTTAC>\n" ^
   279 	     "@@@@@end@@@@@");
   279 	     "@@@@@end@@@@@");
   281 (*. UNCHANGED: the pos' of the active formula autocalculate has been applied at
   281 (*. UNCHANGED: the pos' of the active formula autocalculate has been applied at
   282     DELETED:   last pos' of the succesional sequence of formulae prob. deleted
   282     DELETED:   last pos' of the succesional sequence of formulae prob. deleted
   283     GENERATED: the pos' of the new active formula
   283     GENERATED: the pos' of the new active formula
   284 .*)
   284 .*)
   285 fun autocalculateOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') = 
   285 fun autocalculateOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') = 
   286     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   286     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   287 	     "<AUTOCALC>\n" ^
   287 	     "<AUTOCALC>\n" ^
   288 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   288 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   289 	     "  <CALCCHANGED>\n" ^
   289 	     "  <CALCCHANGED>\n" ^
   290 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   290 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   291 	     pos'2xml (2*i) ("DELETED", del) ^ 
   291 	     pos'2xml (2*i) ("DELETED", del) ^ 
   294 	     "</AUTOCALC>\n" ^
   294 	     "</AUTOCALC>\n" ^
   295 	     "@@@@@end@@@@@");
   295 	     "@@@@@end@@@@@");
   296 (* autocalculate2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
   296 (* autocalculate2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
   297    *)
   297    *)
   298 fun autocalculateERROR2xml (cI:calcID) e = 
   298 fun autocalculateERROR2xml (cI:calcID) e = 
   299     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   299     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   300 	     "<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
   300 	     "<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
   301 	     "@@@@@end@@@@@");
   301 	     "@@@@@end@@@@@");
   302 
   302 
   303 fun interStepsOK (cI:calcID) (*pos'forms*) (old:pos') (del:pos') (new:pos') =
   303 fun interStepsOK (cI:calcID) (*pos'forms*) (old:pos') (del:pos') (new:pos') =
   304     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   304     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   305 	     "<INTERSTEPS>\n" ^
   305 	     "<INTERSTEPS>\n" ^
   306 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   306 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   307 	     "  <CALCCHANGED>\n" ^
   307 	     "  <CALCCHANGED>\n" ^
   308 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   308 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 
   309 	     pos'2xml (2*i) ("DELETED", del) ^ 
   309 	     pos'2xml (2*i) ("DELETED", del) ^ 
   310 	     pos'2xml (2*i) ("GENERATED", new) ^ 
   310 	     pos'2xml (2*i) ("GENERATED", new) ^ 
   311 	     "  </CALCCHANGED>\n" ^
   311 	     "  </CALCCHANGED>\n" ^
   312 	     "</INTERSTEPS>\n" ^
   312 	     "</INTERSTEPS>\n" ^
   313 	     "@@@@@end@@@@@");
   313 	     "@@@@@end@@@@@");
   314 fun interStepsERROR (cI:calcID) e =
   314 fun interStepsERROR (cI:calcID) e =
   315     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   315     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   316 	     "  <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
   316 	     "  <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
   317 	     "@@@@@end@@@@@");
   317 	     "@@@@@end@@@@@");
   318 
   318 
   319 fun modifycalcheadOK2xml (cI:calcID) (chd as (complete,p_,_,_,_,_):ocalhd) =
   319 fun modifycalcheadOK2xml (cI:calcID) (chd as (complete,p_,_,_,_,_):ocalhd) =
   320     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   320     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   321 	     "<MODIFYCALCHEAD>\n" ^
   321 	     "<MODIFYCALCHEAD>\n" ^
   322 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   322 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   323 	     "  <STATUS> "^(if complete then "complete" 
   323 	     "  <STATUS> "^(if complete then "complete" 
   324 			    else "incomplete")^ "</STATUS>\n"^
   324 			    else "incomplete")^ "</STATUS>\n"^
   325 	     modspec2xml i chd^
   325 	     modspec2xml i chd^
   327 	     "@@@@@end@@@@@");
   327 	     "@@@@@end@@@@@");
   328 
   328 
   329 (* val (cI, contthy) = (cI, (context_thy (pt,pos) tac));
   329 (* val (cI, contthy) = (cI, (context_thy (pt,pos) tac));
   330    *)
   330    *)
   331 fun contextthyOK2xml cI contthy = 
   331 fun contextthyOK2xml cI contthy = 
   332     tracing ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   332     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
   333 	     "<CONTEXTTHY>\n" ^
   333 	     "<CONTEXTTHY>\n" ^
   334 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   334 	     "  <CALCID> "^string_of_int cI^" </CALCID>\n" ^
   335 	     contthy2xml i contthy ^
   335 	     contthy2xml i contthy ^
   336 	     "</CONTEXTTHY>\n" ^
   336 	     "</CONTEXTTHY>\n" ^
   337 	     "@@@@@end@@@@@");
   337 	     "@@@@@end@@@@@");
   338 
   338 
   339 (*
   339 (*
   340 fun contextthyNO2xml guh = 
   340 fun contextthyNO2xml guh = 
   341     tracing (datatypes.contextthyNO2xml 0 guh);
   341     writeln (datatypes.contextthyNO2xml 0 guh);
   342 *)
   342 *)