29 val inputFillFormula: calcID -> string -> XML.tree |
29 val inputFillFormula: calcID -> string -> XML.tree |
30 val interSteps : calcID -> Pos.pos' -> XML.tree |
30 val interSteps : calcID -> Pos.pos' -> XML.tree |
31 val Iterator : calcID -> XML.tree |
31 val Iterator : calcID -> XML.tree |
32 val IteratorTEST : calcID -> iterID |
32 val IteratorTEST : calcID -> iterID |
33 val modelProblem : calcID -> XML.tree |
33 val modelProblem : calcID -> XML.tree |
34 val modifyCalcHead : calcID -> Input_Spec.icalhd -> XML.tree |
34 val modifyCalcHead : calcID -> P_Specific.icalhd -> XML.tree |
35 val moveActiveCalcHead : calcID -> XML.tree |
35 val moveActiveCalcHead : calcID -> XML.tree |
36 val moveActiveDown : calcID -> XML.tree |
36 val moveActiveDown : calcID -> XML.tree |
37 val moveActiveFormula : calcID -> Pos.pos' -> XML.tree |
37 val moveActiveFormula : calcID -> Pos.pos' -> XML.tree |
38 val moveActiveLevelDown : calcID -> XML.tree |
38 val moveActiveLevelDown : calcID -> XML.tree |
39 val moveActiveLevelUp : calcID -> XML.tree |
39 val moveActiveLevelUp : calcID -> XML.tree |
71 format accepted by Isabelle. |
71 format accepted by Isabelle. |
72 encode "^" ---> "^^^"; see Knowledge/Atools.thy; |
72 encode "^" ---> "^^^"; see Knowledge/Atools.thy; |
73 called for each cterm', icalhd, fmz in this interface; |
73 called for each cterm', icalhd, fmz in this interface; |
74 + see "fun en/decode" in /mathml.sml *) |
74 + see "fun en/decode" in /mathml.sml *) |
75 fun encode_imodel imodel = |
75 fun encode_imodel imodel = |
76 let fun enc (Input_Spec.Given ifos) = Input_Spec.Given (map encode ifos) |
76 let fun enc (P_Specific.Given ifos) = P_Specific.Given (map encode ifos) |
77 | enc (Input_Spec.Find ifos) = Input_Spec.Find (map encode ifos) |
77 | enc (P_Specific.Find ifos) = P_Specific.Find (map encode ifos) |
78 | enc (Input_Spec.Relate ifos) = Input_Spec.Relate (map encode ifos) |
78 | enc (P_Specific.Relate ifos) = P_Specific.Relate (map encode ifos) |
79 in map enc imodel:Input_Spec.imodel end; |
79 in map enc imodel:P_Specific.imodel end; |
80 fun encode_icalhd ((pos', headl, imodel, pos_, spec) : Input_Spec.icalhd) = |
80 fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Specific.icalhd) = |
81 (pos', encode headl, encode_imodel imodel, pos_, spec) : Input_Spec.icalhd; |
81 (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Specific.icalhd; |
82 fun encode_fmz (ifos, spec) = (map encode ifos, spec); |
82 fun encode_fmz (ifos, spec) = (map encode ifos, spec); |
83 |
83 |
84 |
84 |
85 (***. CalcTree .***) |
85 (***. CalcTree .***) |
86 |
86 |
286 | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos |
286 | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos |
287 end |
287 end |
288 end) |
288 end) |
289 handle _ => sysERROR2xml cI "error in kernel 8"; |
289 handle _ => sysERROR2xml cI "error in kernel 8"; |
290 |
290 |
291 fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : Input_Spec.icalhd) = |
291 fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Specific.icalhd) = |
292 (let |
292 (let |
293 val ((pt,_),_) = get_calc cI |
293 val ((pt,_),_) = get_calc cI |
294 val (pt, chd as (_,p_,_,_,_,_)) = Input_Spec.input_icalhd pt ichd |
294 val (pt, chd as (_,p_,_,_,_,_)) = P_Specific.input_icalhd pt ichd |
295 in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end) |
295 in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end) |
296 handle _ => sysERROR2xml cI "error in kernel 9"; |
296 handle _ => sysERROR2xml cI "error in kernel 9"; |
297 |
297 |
298 (* at the activeFormula set the Model, the Guard and the Specification to empty |
298 (* at the activeFormula set the Model, the Guard and the Specification to empty |
299 and return a CalcHead; the 'origin' remains (for reconstructing all that) *) |
299 and return a CalcHead; the 'origin' remains (for reconstructing all that) *) |