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