1.1 --- a/src/Tools/isac/Frontend/interface.sml Tue May 19 10:57:38 2015 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Tue May 19 12:38:32 2015 +0200
1.3 @@ -11,7 +11,7 @@
1.4
1.5 signature INTERFACE =
1.6 sig
1.7 - val CalcTree : fmz list -> unit
1.8 + val CalcTree : fmz list -> XML.tree
1.9 val DEconstrCalcTree : calcID -> unit
1.10 val Iterator : calcID -> XML.tree
1.11 val IteratorTEST : calcID -> iterID
1.12 @@ -22,28 +22,28 @@
1.13 val fetchProposedTactic : calcID -> unit
1.14 val applyTactic : calcID -> pos' -> tac -> unit
1.15 val getAccumulatedAsms : calcID -> pos' -> unit
1.16 - val getActiveFormula : calcID -> unit
1.17 + val getActiveFormula : calcID -> XML.tree
1.18 val getAssumptions : calcID -> pos' -> unit
1.19 val initContext : calcID -> ketype -> pos' -> unit
1.20 val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> unit
1.21 val getTactic : calcID -> pos' -> unit
1.22 val interSteps : calcID -> pos' -> unit
1.23 val modifyCalcHead : calcID -> icalhd -> unit
1.24 - val moveActiveCalcHead : calcID -> unit
1.25 - val moveActiveDown : calcID -> unit
1.26 + val moveActiveCalcHead : calcID -> XML.tree
1.27 + val moveActiveDown : calcID -> XML.tree
1.28 val moveActiveDownTEST : calcID -> unit
1.29 - val moveActiveFormula : calcID -> pos' -> unit
1.30 - val moveActiveLevelDown : calcID -> unit
1.31 - val moveActiveLevelUp : calcID -> unit
1.32 - val moveActiveRoot : calcID -> unit
1.33 + val moveActiveFormula : calcID -> pos' -> XML.tree
1.34 + val moveActiveLevelDown : calcID -> XML.tree
1.35 + val moveActiveLevelUp : calcID -> XML.tree
1.36 + val moveActiveRoot : calcID -> XML.tree
1.37 val moveActiveRootTEST : calcID -> unit
1.38 - val moveActiveUp : calcID -> unit
1.39 - val moveCalcHead : calcID -> pos' -> unit
1.40 - val moveDown : calcID -> pos' -> unit
1.41 - val moveLevelDown : calcID -> pos' -> unit
1.42 - val moveLevelUp : calcID -> pos' -> unit
1.43 - val moveRoot : calcID -> unit
1.44 - val moveUp : calcID -> pos' -> unit
1.45 + val moveActiveUp : calcID -> XML.tree
1.46 + val moveCalcHead : calcID -> pos' -> XML.tree
1.47 + val moveDown : calcID -> pos' -> XML.tree
1.48 + val moveLevelDown : calcID -> pos' -> XML.tree
1.49 + val moveLevelUp : calcID -> pos' -> XML.tree
1.50 + val moveRoot : calcID -> XML.tree
1.51 + val moveUp : calcID -> pos' -> XML.tree
1.52 val refFormula : calcID -> pos' -> unit
1.53 val replaceFormula : calcID -> cterm' -> unit
1.54 val resetCalcHead : calcID -> unit
1.55 @@ -111,7 +111,7 @@
1.56 (*FIXME.WN.8.03: error-handling missing*)
1.57 val cI = add_calc cs
1.58 in calctreeOK2xml cI end)
1.59 - handle _ => sysERROR2xml 0 "error in kernel";
1.60 + handle _ => sysERROR2xmlTODO 0 "error in kernel";
1.61
1.62 fun DEconstrCalcTree (cI:calcID) =
1.63 deconstructcalctreeOK2xml (del_calc cI);
1.64 @@ -122,7 +122,7 @@
1.65 fun moveActiveFormula (cI:calcID) (p:pos') =
1.66 let val ((pt,_),_) = get_calc cI
1.67 in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)
1.68 - else sysERROR2xml cI "frontend sends a non-existing pos" end;
1.69 + else sysERROR2xmlTODO cI "frontend sends a non-existing pos" end;
1.70
1.71 (*. set the next tactic to be applied: dont't change the calc-tree,
1.72 but remember the envisaged changes for fun autoCalculate;
1.73 @@ -564,10 +564,10 @@
1.74 fun moveActiveRoot cI =
1.75 (let val _ = upd_ipos cI 1 ([],Pbl)
1.76 in iteratorOK2xml cI ([],Pbl) end)
1.77 - handle e => sysERROR2xml cI "error in kernel";
1.78 + handle e => sysERROR2xmlTODO cI "error in kernel";
1.79 fun moveRoot cI =
1.80 (iteratorOK2xml cI ([],Pbl))
1.81 - handle e => sysERROR2xml cI "";
1.82 + handle e => sysERROR2xmlTODO cI "";
1.83 fun moveActiveRootTEST cI =
1.84 (let val _ = upd_ipos cI 1 ([],Pbl)
1.85 in (*iteratorOK2xml cI ([],Pbl)*)() end)
1.86 @@ -587,7 +587,7 @@
1.87 val _ = upd_ipos cI 1 ip'
1.88 in iteratorOK2xml cI ip' end)
1.89 handle (PTREE e) => iteratorERROR2xml cI)
1.90 - handle _ => sysERROR2xml cI "error in kernel";
1.91 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.92 fun moveDown cI (p:pos') =
1.93 ((let val ((pt,_),_) = get_calc cI
1.94 (* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
1.95 @@ -598,7 +598,7 @@
1.96 val ip' = move_dn [] pt p
1.97 in iteratorOK2xml cI ip' end)
1.98 handle (PTREE e) => iteratorERROR2xml cI)
1.99 - handle _ => sysERROR2xml cI "error in kernel";
1.100 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.101 fun moveActiveDownTEST cI =
1.102 let val ((pt,_),_) = get_calc cI
1.103 val ip = get_pos cI 1
1.104 @@ -613,13 +613,13 @@
1.105 val _ = upd_ipos cI 1 ip'
1.106 in iteratorOK2xml cI ip' end)
1.107 handle (PTREE e) => iteratorERROR2xml cI)
1.108 - handle _ => sysERROR2xml cI "error in kernel";
1.109 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.110 fun moveLevelDown cI (p:pos') =
1.111 ((let val ((pt,_),_) = get_calc cI
1.112 val ip' = movelevel_dn [] pt p
1.113 in iteratorOK2xml cI ip' end)
1.114 handle (PTREE e) => iteratorERROR2xml cI)
1.115 - handle _ => sysERROR2xml cI "error in kernel";
1.116 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.117
1.118 fun moveActiveUp cI =
1.119 ((let val ((pt,_),_) = get_calc cI
1.120 @@ -627,13 +627,13 @@
1.121 val _ = upd_ipos cI 1 ip'
1.122 in iteratorOK2xml cI ip' end)
1.123 handle PTREE e => iteratorERROR2xml cI)
1.124 - handle _ => sysERROR2xml cI "error in kernel";
1.125 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.126 fun moveUp cI (p:pos') =
1.127 ((let val ((pt,_),_) = get_calc cI
1.128 val ip' = move_up [] pt p
1.129 in iteratorOK2xml cI ip' end)
1.130 handle PTREE e => iteratorERROR2xml cI)
1.131 - handle _ => sysERROR2xml cI "error in kernel";
1.132 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.133
1.134 fun moveActiveLevelUp cI =
1.135 ((let val ((pt,_),_) = get_calc cI
1.136 @@ -641,13 +641,13 @@
1.137 val _ = upd_ipos cI 1 ip'
1.138 in iteratorOK2xml cI ip' end)
1.139 handle PTREE e => iteratorERROR2xml cI)
1.140 - handle _ => sysERROR2xml cI "error in kernel";
1.141 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.142 fun moveLevelUp cI (p:pos') =
1.143 ((let val ((pt,_),_) = get_calc cI
1.144 val ip' = movelevel_up [] pt p
1.145 in iteratorOK2xml cI ip' end)
1.146 handle PTREE e => iteratorERROR2xml cI)
1.147 - handle _ => sysERROR2xml cI "error in kernel";
1.148 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.149
1.150 fun moveActiveCalcHead cI =
1.151 ((let val ((pt,_),_) = get_calc cI
1.152 @@ -655,13 +655,13 @@
1.153 val _ = upd_ipos cI 1 ip'
1.154 in iteratorOK2xml cI ip' end)
1.155 handle PTREE e => iteratorERROR2xml cI)
1.156 - handle _ => sysERROR2xml cI "error in kernel";
1.157 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.158 fun moveCalcHead cI (p:pos') =
1.159 ((let val ((pt,_),_) = get_calc cI
1.160 val ip' = movecalchd_up pt p
1.161 in iteratorOK2xml cI ip' end)
1.162 handle PTREE e => iteratorERROR2xml cI)
1.163 - handle _ => sysERROR2xml cI "error in kernel";
1.164 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.165
1.166
1.167 (*.initContext Thy_ is conceptually impossible at [Pbl,Met]
2.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Tue May 19 10:57:38 2015 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Tue May 19 12:38:32 2015 +0200
2.3 @@ -34,12 +34,9 @@
2.4 "@@@@@end@@@@@");
2.5 (*---------------------------------------------------------------------*)
2.6
2.7 -fun calctreeOK2xml (*uI:iterID*) (cI:calcID) =
2.8 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.9 - "<CALCTREE>\n" ^
2.10 - " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.11 - "</CALCTREE>\n" ^
2.12 - "@@@@@end@@@@@");
2.13 +fun calctreeOK2xml (calcid : calcID) =
2.14 + XML.Elem (("CALCTREE", []),
2.15 + [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])
2.16 fun deconstructcalctreeOK2xml (*uI:userID*) (cI:calcID) =
2.17 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.18 "<DELCALC>\n" ^
2.19 @@ -47,20 +44,14 @@
2.20 "</DELCALC>\n" ^
2.21 "@@@@@end@@@@@");
2.22
2.23 -fun iteratorOK2xml (cI:calcID) (p:pos')=
2.24 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.25 - "<CALCITERATOR>\n" ^
2.26 - " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.27 - pos'2xml i ("POSITION", p) ^
2.28 - "</CALCITERATOR>\n" ^
2.29 - "@@@@@end@@@@@");
2.30 -fun iteratorERROR2xml (cI:calcID) =
2.31 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
2.32 - "<CALCITERATOR>\n" ^
2.33 - " <CALCID> "^string_of_int cI^" </CALCID>\n" ^
2.34 - " <ERROR> pos does not exist </ERROR>\n" ^
2.35 - "</CALCITERATOR>\n" ^
2.36 - "@@@@@end@@@@@");
2.37 +fun iteratorOK2xml (calcid : calcID) (p : pos')=
2.38 + XML.Elem (("CALCITERATOR", []),
2.39 + [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.40 + xml_of_pos "POSITION" p])
2.41 +fun iteratorERROR2xml (calcid : calcID) =
2.42 + XML.Elem (("CALCITERATOR", []),
2.43 + [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.44 + XML.Elem (("ERROR", []), [XML.Text " pos does not exist "])])
2.45
2.46 fun sysERROR2xml (cI:calcID) "" =
2.47 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^