1.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Sun Jul 29 16:29:04 2012 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Mon Jul 30 16:41:08 2012 +0200
1.3 @@ -12,10 +12,7 @@
1.4 "@@@@@begin@@@@@\n "^string_of_int uI
1.5 # omit the distinctions APPENDFORMULA, REPLACEFORMULA, ...
1.6 WN071004 these 2 simplifications are begun with CALCMESSAGE
1.7 -
1.8 - use"xmlsrc/interface-xml.sml";
1.9 - use"interface-xml.sml";
1.10 - *)
1.11 +*)
1.12
1.13 type iterID = int;
1.14 type calcID = int;
1.15 @@ -260,16 +257,14 @@
1.16 "</SETNEXTTACTIC>\n" ^
1.17 "@@@@@end@@@@@");
1.18
1.19 -fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac =
1.20 +fun fetchproposedtacticOK2xml (cI:calcID) tac =
1.21 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
1.22 "<NEXTTAC>\n" ^
1.23 " <CALCID> "^string_of_int cI^" </CALCID>\n"^
1.24 tac2xml i tac^
1.25 -(* ^(strs2xml o (map (tac2xml i))) tacs^*)
1.26 "</NEXTTAC>\n" ^
1.27 "@@@@@end@@@@@");
1.28 -(* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));
1.29 - *)
1.30 +
1.31 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e =
1.32 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
1.33 "<NEXTTAC>\n" ^
1.34 @@ -340,8 +335,16 @@
1.35 contthy2xml i contthy ^
1.36 "</CONTEXTTHY>\n" ^
1.37 "@@@@@end@@@@@");
1.38 -
1.39 (*
1.40 fun contextthyNO2xml guh =
1.41 writeln (datatypes.contextthyNO2xml 0 guh);
1.42 *)
1.43 +
1.44 +fun findFillpatterns2xml (cI:calcID) pattIDs =
1.45 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
1.46 + "<FINDFILLPATTERNS>\n" ^
1.47 + " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
1.48 + id2xml 3 pattIDs ^
1.49 + "</FINDFILLPATTERNS>\n" ^
1.50 + "@@@@@end@@@@@");
1.51 +