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