2 imports "~~/src/Tools/isac/Knowledge/Build_Thydata" Protocol.Protocol
5 (* val appendFormula : calcID -> cterm' -> XML.tree *)
6 operation_setup (sequential, bracket, auto) append_form =
9 val (calcid, cterm') = case intree of
10 XML.Elem (("APPENDFORMULA", []), [
11 XML.Elem (("CALCID", []), [XML.Text ci]),
12 form]) => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> UnparseC.term)
13 | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
14 val result = Kernel.appendFormula calcid cterm'
16 handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
18 (* val autoCalculate : calcID -> auto -> XML.tree *)
19 operation_setup autocalculate = \<open>
20 {from_lib = Codec.tree,
22 action = (fn intree =>
24 val (ci, a) = case intree of
25 XML.Elem (("AUTOCALC", []), [
26 XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
27 | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
28 val SOME calcid = TermC.int_opt_of_string ci
29 val auto = xml_to_auto a
30 val result = Kernel.autoCalculate calcid auto
32 handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
34 (* val applyTactic : calcID -> pos' -> tac -> XML.tree *)
35 operation_setup apply_tac = \<open>
36 {from_lib = Codec.tree,
38 action = (fn intree =>
40 val (ci, pos, tac) = case intree of
41 XML.Elem (("AUTOCALC", []), [
42 XML.Elem (("CALCID", []), [XML.Text ci]),
43 pos, tac]) => (TermC.int_of_str ci, xml_to_pos pos, xml_to_tac tac)
44 | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
45 val result = Kernel.applyTactic ci pos tac
47 handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
49 (* val CalcTree : fmz list -> XML.tree *)
50 operation_setup calctree = \<open>
51 {from_lib = Codec.tree,
53 action = (fn intree =>
55 val fmz = case intree of
56 tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
57 | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
58 val result = Kernel.CalcTree fmz
60 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
62 (* val checkContext : calcID -> pos' -> guh -> XML.tree *)
63 operation_setup check_ctxt = \<open>
64 {from_lib = Codec.tree,
66 action = (fn intree =>
68 val (ci, pos, guh) = case intree of
69 XML.Elem (("CONTEXTTHY", []), [
70 XML.Elem (("CALCID", []), [XML.Text ci]),
71 pos as XML.Elem (("POSITION", []), _),
72 XML.Elem (("GUH", []), [XML.Text guh])])
73 => (TermC.int_of_str ci, xml_to_pos pos, guh)
74 | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
75 val result = Kernel.checkContext ci pos guh
77 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
79 (* val DEconstrCalcTree : calcID -> XML.tree *)
80 operation_setup deconstrcalctree = \<open>
81 {from_lib = Codec.int,
83 action = (fn calcid =>
85 val result = Kernel.DEconstrCalcTree calcid
86 in result end)}\<close>
88 (* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
89 operation_setup fetch_applicable_tacs = \<open>
90 {from_lib = Codec.tree,
92 action = (fn intree =>
94 val (ci, i, pos) = case intree of
95 XML.Elem (("APPLICABLETACTICS", []), [
96 XML.Elem (("CALCID", []), [XML.Text ci]),
97 XML.Elem (("INT", []), [XML.Text i]),
98 pos as XML.Elem (("POSITION", []), _)])
99 => (TermC.int_of_str ci, TermC.int_of_str i, xml_to_pos pos)
100 | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
101 val result = Kernel.fetchApplicableTactics ci i pos
103 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
105 (* val fetchProposedTactic : calcID -> XML.tree *)
106 operation_setup fetch_proposed_tac = \<open>
107 {from_lib = Codec.tree,
109 action = (fn intree =>
111 val (ci) = case intree of
112 XML.Elem (("NEXTTAC", []), [
113 XML.Elem (("CALCID", []), [XML.Text ci])]) => (TermC.int_of_str ci)
114 | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
115 val result = Kernel.fetchProposedTactic ci
117 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
119 (* val findFillpatterns : calcID -> errpatID -> XML.tree *)
120 operation_setup find_fill_patts = \<open>
121 {from_lib = Codec.tree,
123 action = (fn intree =>
125 val (ci, err_pat_id) = case intree of
126 XML.Elem (("FINDFILLPATTERNS", []), [
127 XML.Elem (("CALCID", []), [XML.Text ci]),
128 XML.Elem (("STRING", []), [XML.Text err_pat_id])])
129 => (TermC.int_of_str ci, err_pat_id)
130 | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
131 val result = Kernel.findFillpatterns ci err_pat_id
133 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
135 (* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)
136 operation_setup get_accumulated_asms = \<open>
137 {from_lib = Codec.tree,
139 action = (fn intree =>
141 val (ci, pos) = case intree of
142 XML.Elem (("GETASSUMPTIONS", []), [
143 XML.Elem (("CALCID", []), [XML.Text ci]),
144 pos as XML.Elem (("POSITION", []), _)])
145 => (TermC.int_of_str ci, xml_to_pos pos)
146 | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
147 val result = Kernel.getAccumulatedAsms ci pos
149 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
151 (* val getActiveFormula : calcID -> XML.tree *)
152 operation_setup get_active_form = \<open>
153 {from_lib = Codec.tree,
155 action = (fn intree =>
157 val (ci) = case intree of
158 XML.Elem (("CALCITERATOR", []), [
159 XML.Elem (("CALCID", []), [XML.Text ci])])
160 => (TermC.int_of_str ci)
161 | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
162 val result = Kernel.getActiveFormula ci
164 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
166 (* val getAssumptions : calcID -> pos' -> XML.tree *)
167 operation_setup get_asms = \<open>
168 {from_lib = Codec.tree,
170 action = (fn intree =>
172 val (ci, pos) = case intree of
173 XML.Elem (("APPLICABLETACTICS", []), [
174 XML.Elem (("CALCID", []), [XML.Text ci]),
175 pos as XML.Elem (("POSITION", []), _)])
176 => (TermC.int_of_str ci, xml_to_pos pos)
177 | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
178 val result = Kernel.getAssumptions ci pos
180 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
182 (* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)
183 operation_setup getformulaefromto = \<open>
184 {from_lib = Codec.tree,
186 action = (fn intree =>
188 val (calcid, from, to, level, rules) = case intree of
189 XML.Elem (("GETFORMULAEFROMTO", []), [
190 XML.Elem (("CALCID", []), [XML.Text calcid]),
191 from as XML.Elem (("POSITION", []), [
192 XML.Elem (("INTLIST", []), _),
193 XML.Elem (("POS", []), [XML.Text _])]),
194 to as XML.Elem (("POSITION", []), [
195 XML.Elem (("INTLIST", []), _),
196 XML.Elem (("POS", []), [XML.Text _])]),
197 XML.Elem (("INT", []), [XML.Text level]),
198 XML.Elem (("BOOL", []), [XML.Text rules])])
199 => (TermC.int_of_str calcid, xml_to_pos from, xml_to_pos to, TermC.int_of_str level, string_to_bool rules)
200 | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
201 val result = Kernel.getFormulaeFromTo calcid from to level rules
203 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
205 (* val getTactic : calcID -> pos' -> XML.tree *)
206 operation_setup get_tac = \<open>
207 {from_lib = Codec.tree,
209 action = (fn intree =>
211 val (ci, pos) = case intree of
212 XML.Elem (("GETTACTIC", []), [
213 XML.Elem (("CALCID", []), [XML.Text ci]),
214 pos as XML.Elem (("POSITION", []), _)])
215 => (TermC.int_of_str ci, xml_to_pos pos)
216 | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
217 val result = Kernel.getTactic ci pos
219 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
221 (* val initContext : calcID -> ketype -> pos' -> XML.tree *)
222 operation_setup init_ctxt = \<open>
223 {from_lib = Codec.tree,
225 action = (fn intree =>
227 val (ci, ketype, pos) = case intree of
228 XML.Elem (("INITCONTEXT", []), [
229 XML.Elem (("CALCID", []), [XML.Text ci]),
230 ketype as XML.Elem (("KETYPE", []), _),
231 pos as XML.Elem (("POSITION", []), _)])
232 => (TermC.int_of_str ci, xml_to_ketype ketype, xml_to_pos pos)
233 | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
234 val result = Kernel.initContext ci ketype pos
236 handle ERROR msg => sysERROR2xml 4711 msg)
237 handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
239 (* val inputFillFormula: calcID -> string -> XML.tree *)
240 operation_setup input_fill_form = \<open>
241 {from_lib = Codec.tree,
243 action = (fn intree =>
245 val (ci, str) = case intree of
246 XML.Elem (("AUTOCALC", []), [
247 XML.Elem (("CALCID", []), [XML.Text ci]),
248 XML.Elem (("STRING", []), [XML.Text str])])
249 => (TermC.int_of_str ci, str)
250 | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
251 val result = Kernel.inputFillFormula ci str
253 handle ERROR msg => message2xml 4711 msg)}\<close>
255 (* val interSteps : calcID -> pos' -> XML.tree *)
256 operation_setup inter_steps = \<open>
257 {from_lib = Codec.tree,
259 action = (fn intree =>
261 val (ci, pos) = case intree of
262 XML.Elem (("INTERSTEPS", []), [
263 XML.Elem (("CALCID", []), [XML.Text ci]),
264 pos as XML.Elem (("POSITION", []), _)])
265 => (TermC.int_of_str ci, xml_to_pos pos)
266 | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
267 val result = Kernel.interSteps ci pos
269 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
271 (* val Iterator : calcID -> XML.tree *)
272 operation_setup iterator = \<open>
273 {from_lib = Codec.int,
275 action = (fn calcid =>
277 val result = Kernel.Iterator calcid
278 in result end)}\<close>
280 (* val IteratorTEST : calcID -> iterID *)
282 (* val modelProblem : calcID -> XML.tree *)
283 operation_setup model_pbl = \<open>
284 {from_lib = Codec.tree,
286 action = (fn intree =>
288 val (ci) = case intree of
289 XML.Elem (("MODIFYCALCHEAD", []), [
290 XML.Elem (("CALCID", []), [XML.Text ci])])
291 => (TermC.int_of_str ci)
292 | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
293 val result = Kernel.modelProblem ci
295 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
297 (* val modifyCalcHead : calcID -> icalhd -> XML.tree *)
298 operation_setup modify_calchead = \<open>
299 {from_lib = Codec.tree,
301 action = (fn intree =>
303 val (ci, icalhd) = case intree of
304 XML.Elem (("MODIFYCALCHEAD", []), [
305 XML.Elem (("CALCID", []), [XML.Text ci]),
307 => (TermC.int_of_str ci, xml_to_icalhd icalhd)
308 | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
309 val result = Kernel.modifyCalcHead ci icalhd
311 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
313 (* val moveActiveCalcHead : calcID -> XML.tree *)
314 operation_setup move_active_calchead = \<open>
315 {from_lib = Codec.tree,
317 action = (fn intree =>
319 val (ci) = case intree of
320 XML.Elem (("CALCITERATOR", []), [
321 XML.Elem (("CALCID", []), [XML.Text ci])])
322 => (TermC.int_of_str ci)
323 | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
324 val result = Kernel.moveActiveCalcHead ci
326 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
328 (* val moveActiveDown : calcID -> XML.tree *)
329 operation_setup move_active_down = \<open>
330 {from_lib = Codec.tree,
332 action = (fn intree =>
334 val (ci) = case intree of
335 XML.Elem (("CALCITERATOR", []), [
336 XML.Elem (("CALCID", []), [XML.Text ci])])
337 => (TermC.int_of_str ci)
338 | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
339 val result = Kernel.moveActiveDown ci
341 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
343 (* val moveActiveFormula : calcID -> pos' -> XML.tree *)
344 operation_setup move_active_form = \<open>
345 {from_lib = Codec.tree,
347 action = (fn intree =>
349 val (ci, pos) = case intree of
350 XML.Elem (("CALCITERATOR", []), [
351 XML.Elem (("CALCID", []), [XML.Text ci]),
352 pos as XML.Elem (("POSITION", []), _)])
353 => (TermC.int_of_str ci, xml_to_pos pos)
354 | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
355 val result = Kernel.moveActiveFormula ci pos
357 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
359 (* val moveActiveLevelDown : calcID -> XML.tree *)
360 operation_setup move_active_levdown = \<open>
361 {from_lib = Codec.tree,
363 action = (fn intree =>
365 val (ci) = case intree of
366 XML.Elem (("CALCITERATOR", []), [
367 XML.Elem (("CALCID", []), [XML.Text ci])])
368 => (TermC.int_of_str ci)
369 | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
370 val result = Kernel.moveActiveLevelDown ci
372 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
374 (* val moveActiveLevelUp : calcID -> XML.tree *)
375 operation_setup move_active_levup = \<open>
376 {from_lib = Codec.tree,
378 action = (fn intree =>
380 val (ci) = case intree of
381 XML.Elem (("CALCITERATOR", []), [
382 XML.Elem (("CALCID", []), [XML.Text ci])])
383 => (TermC.int_of_str ci)
384 | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
385 val result = Kernel.moveActiveLevelUp ci
387 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
389 (* val moveActiveRoot : calcID -> XML.tree *)
390 operation_setup moveactiveroot = \<open>
391 {from_lib = Codec.int,
393 action = (fn calcid =>
395 val result = Kernel.moveActiveRoot calcid
396 in result end)}\<close>
398 (* val moveActiveRootTEST : calcID -> XML.tree *)
400 (* val moveActiveUp : calcID -> XML.tree *)
401 operation_setup move_active_up = \<open>
402 {from_lib = Codec.tree,
404 action = (fn intree =>
406 val (ci) = case intree of
407 XML.Elem (("CALCITERATOR", []), [
408 XML.Elem (("CALCID", []), [XML.Text ci])])
409 => (TermC.int_of_str ci)
410 | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
411 val result = Kernel.moveActiveUp ci
413 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
415 (* val moveCalcHead : calcID -> pos' -> XML.tree *)
416 operation_setup move_calchead = \<open>
417 {from_lib = Codec.tree,
419 action = (fn intree =>
421 val (ci, pos) = case intree of
422 XML.Elem (("CALCITERATOR", []), [
423 XML.Elem (("CALCID", []), [XML.Text ci]),
424 pos as XML.Elem (("POSITION", []), _)])
425 => (TermC.int_of_str ci, xml_to_pos pos)
426 | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
427 val result = Kernel.moveCalcHead ci pos
429 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
431 (* val moveDown : calcID -> pos' -> XML.tree *)
432 operation_setup move_down = \<open>
433 {from_lib = Codec.tree,
435 action = (fn intree =>
437 val (ci, pos) = case intree of
438 XML.Elem (("CALCITERATOR", []), [
439 XML.Elem (("CALCID", []), [XML.Text ci]),
440 pos as XML.Elem (("POSITION", []), _)])
441 => (TermC.int_of_str ci, xml_to_pos pos)
442 | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
443 val result = Kernel.moveDown ci pos
445 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
447 (* val moveLevelDown : calcID -> pos' -> XML.tree *)
448 operation_setup move_levdn = \<open>
449 {from_lib = Codec.tree,
451 action = (fn intree =>
453 val (ci, pos) = case intree of
454 XML.Elem (("CALCITERATOR", []), [
455 XML.Elem (("CALCID", []), [XML.Text ci]),
456 pos as XML.Elem (("POSITION", []), _)])
457 => (TermC.int_of_str ci, xml_to_pos pos)
458 | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
459 val result = Kernel.moveLevelDown ci pos
461 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
463 (* val moveLevelUp : calcID -> pos' -> XML.tree *)
464 operation_setup move_levup = \<open>
465 {from_lib = Codec.tree,
467 action = (fn intree =>
469 val (ci, pos) = case intree of
470 XML.Elem (("CALCITERATOR", []), [
471 XML.Elem (("CALCID", []), [XML.Text ci]),
472 pos as XML.Elem (("POSITION", []), _)])
473 => (TermC.int_of_str ci, xml_to_pos pos)
474 | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
475 val result = Kernel.moveLevelUp ci pos
477 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
479 (* val moveRoot : calcID -> XML.tree *)
480 operation_setup move_root = \<open>
481 {from_lib = Codec.tree,
483 action = (fn intree =>
485 val (ci) = case intree of
486 XML.Elem (("CALCITERATOR", []), [
487 XML.Elem (("CALCID", []), [XML.Text ci])])
488 => (TermC.int_of_str ci)
489 | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
490 val result = Kernel.moveRoot ci
492 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
494 (* val moveUp : calcID -> pos' -> XML.tree *)
495 operation_setup move_up = \<open>
496 {from_lib = Codec.tree,
498 action = (fn intree =>
500 val (ci, pos) = case intree of
501 XML.Elem (("CALCITERATOR", []), [
502 XML.Elem (("CALCID", []), [XML.Text ci]),
503 pos as XML.Elem (("POSITION", []), _)])
504 => (TermC.int_of_str ci, xml_to_pos pos)
505 | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
506 val result = Kernel.moveUp ci pos
508 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
510 (* val refFormula : calcID -> pos' -> XML.tree *)
511 operation_setup refformula = \<open>
512 {from_lib = Codec.tree,
514 action = (fn intree =>
516 val (ci, p) = case intree of
517 XML.Elem (("REFFORMULA", []), [
518 XML.Elem (("CALCID", []), [XML.Text ci]), p])
520 | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
521 val SOME calcid = TermC.int_opt_of_string ci
522 val pos = xml_to_pos p
523 val result = Kernel.refFormula calcid pos
525 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
528 val refineProblem : calcID -> pos' -> guh -> XML.tree *)
529 operation_setup refine_pbl = \<open>
530 {from_lib = Codec.tree,
532 action = (fn intree =>
534 val (ci, pos, guh) = case intree of
535 XML.Elem (("CONTEXTPBL", []), [
536 XML.Elem (("CALCID", []), [XML.Text ci]),
537 pos as XML.Elem (("POSITION", []), _),
538 XML.Elem (("GUH", []), [XML.Text guh])])
539 => (TermC.int_of_str ci, xml_to_pos pos, guh)
540 | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
541 val result = Kernel.refineProblem ci pos guh
543 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
545 (* val replaceFormula : calcID -> cterm' -> XML.tree *)
546 operation_setup replace_form = \<open>
547 {from_lib = Codec.tree,
549 action = (fn intree =>
551 val (calcid, cterm') = case intree of
552 XML.Elem (("REPLACEFORMULA", []), [
553 XML.Elem (("CALCID", []), [XML.Text ci]), form])
554 => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> UnparseC.term)
555 | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
556 val result = Kernel.replaceFormula calcid cterm'
558 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
560 (* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)
561 operation_setup request_fill_form = \<open>
562 {from_lib = Codec.tree,
564 action = (fn intree =>
566 val (ci, errpat_id, fillpat_id) = case intree of
567 XML.Elem (("AUTOCALC", []), [
568 XML.Elem (("CALCID", []), [XML.Text ci]),
569 XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),
570 XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
571 => (TermC.int_of_str ci, errpat_id, fillpat_id)
572 | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
573 val result = Kernel.requestFillformula ci (errpat_id, fillpat_id)
575 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
577 (* val resetCalcHead : calcID -> XML.tree *)
578 operation_setup reset_calchead = \<open>
579 {from_lib = Codec.tree,
581 action = (fn intree =>
583 val (ci) = case intree of
584 XML.Elem (("MODIFYCALCHEAD", []), [
585 XML.Elem (("CALCID", []), [XML.Text ci])])
586 => (TermC.int_of_str ci)
587 | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
588 val result = Kernel.resetCalcHead ci
590 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
592 (* val setContext : calcID -> pos' -> guh -> XML.tree *)
593 operation_setup set_ctxt = \<open>
594 {from_lib = Codec.tree,
596 action = (fn intree =>
598 val (ci, pos, guh) = case intree of
599 XML.Elem (("CONTEXT", []), [
600 XML.Elem (("CALCID", []), [XML.Text ci]),
601 pos as XML.Elem (("POSITION", []), _),
602 XML.Elem (("GUH", []), [XML.Text guh])])
603 => (TermC.int_of_str ci, xml_to_pos pos, guh)
604 | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
605 val result = Kernel.setContext ci pos guh
607 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
609 (*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)
611 (* val setMethod : calcID -> metID -> XML.tree *)
612 operation_setup set_met = \<open>
613 {from_lib = Codec.tree,
615 action = (fn intree =>
617 val (ci, met_id) = case intree of
618 XML.Elem (("MODIFYCALCHEAD", []), [
619 XML.Elem (("CALCID", []), [XML.Text ci]),
620 XML.Elem (("METHODID", []), [met_id])])
621 => (TermC.int_of_str ci, xml_to_strs met_id)
622 | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
623 val result = Kernel.setMethod ci met_id
625 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
627 (* val setNextTactic : calcID -> tac -> XML.tree *)
628 operation_setup set_next_tac = \<open>
629 {from_lib = Codec.tree,
631 action = (fn intree =>
633 val (ci, tac) = case intree of
634 XML.Elem (("SETNEXTTACTIC", []), [
635 XML.Elem (("CALCID", []), [XML.Text ci]),
637 => (TermC.int_of_str ci, xml_to_tac tac)
638 | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
639 val result = Kernel.setNextTactic ci tac
641 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
643 (*\\===^^^ TODO ================================================================///////////////*)
645 (* val setProblem : calcID -> pblID -> XML.tree *)
646 operation_setup set_pbl = \<open>
647 {from_lib = Codec.tree,
649 action = (fn intree =>
651 val (ci, pbl_id) = case intree of
652 XML.Elem (("MODIFYCALCHEAD", []), [
653 XML.Elem (("CALCID", []), [XML.Text ci]),
654 XML.Elem (("PROBLEMID", []), [pbl_id])])
655 => (TermC.int_of_str ci, xml_to_strs pbl_id)
656 | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
657 val result = Kernel.setProblem ci pbl_id
659 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
661 (* val setTheory : calcID -> thyID -> XML.tree *)
662 operation_setup set_thy = \<open>
663 {from_lib = Codec.tree,
665 action = (fn intree =>
667 val (ci, thy_id) = case intree of
668 XML.Elem (("MODIFYCALCHEAD", []), [
669 XML.Elem (("CALCID", []), [XML.Text ci]),
670 XML.Elem (("THEORYID", []), [XML.Text thy_id])])
671 => (TermC.int_of_str ci, thy_id)
672 | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
673 val result = Kernel.setTheory ci thy_id
675 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
677 (* for inital java-tests/isac/bridge/TestTerm.scala *)
678 operation_setup make_int = \<open>
679 {from_lib = Codec.unit,
681 action = (fn _ => HOLogic.mk_number @{typ int} 3)}
684 (* passes libisabelle term in both directions;
685 the use of direction isac-java \<longrightarrow> Isabelle/Isac is a future design question *)
686 operation_setup test_term_transfer = \<open>
687 {from_lib = Codec.tree,
689 action = (fn intree =>
691 val t = case intree of
692 XML.Elem (("MATHML", []), [
693 XML.Elem (("ISA", []), [XML.Text _]),
694 XML.Elem (("TERM", []), [xt])])
695 => xt |> Codec.decode Codec.term |> Codec.the_success
696 | tree => raise ERROR ("test_term_transfer: WRONG intree = " ^ xmlstr 0 tree)
697 val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
698 in xml_of_term_NEW test_out end)
699 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
701 operation_setup test_term_one_way = \<open>
702 {from_lib = Codec.string,
704 action = (fn instr =>
706 val t = instr |> TermC.parse @{theory} |> the |> Thm.term_of
707 val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
708 in xml_of_term_NEW test_out end)
709 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
711 (* tool for creating libisabelle's terms *)
712 operation_setup scalaterm_of_string = \<open>
713 {from_lib = Codec.string,
715 action = (fn instr =>
717 val termopt = TermC.parseNEW (Proof_Context.init_global @{theory}) instr
719 case TermC.parseNEW (Proof_Context.init_global @{theory}) instr of
720 SOME term => xml_of_term_NEW term
721 | NONE => sysERROR2xml 4711 ("*** syntax ERROR in: " ^ instr)