1.1 --- a/src/Tools/isac/Frontend/Frontend.thy Sun May 31 10:31:53 2015 +0200
1.2 +++ b/src/Tools/isac/Frontend/Frontend.thy Sun May 31 10:37:31 2015 +0200
1.3 @@ -13,10 +13,4 @@
1.4
1.5 ML_file "~~/src/Tools/isac/print_exn_G.sml"
1.6
1.7 -ML {*
1.8 -*} ML {*
1.9 -*} ML {*
1.10 -*} ML {*
1.11 -*}
1.12 -
1.13 end
1.14 \ No newline at end of file
2.1 --- a/src/Tools/isac/Frontend/interface.sml Sun May 31 10:31:53 2015 +0200
2.2 +++ b/src/Tools/isac/Frontend/interface.sml Sun May 31 10:37:31 2015 +0200
2.3 @@ -379,9 +379,9 @@
2.4 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
2.5 "thy_" =>
2.6 if member op = [Pbl,Met] p_
2.7 - then message2xmlTODO cI "thy-context not to calchead"
2.8 - else if ip = ([],Res) then message2xmlTODO cI "no thy-context at result"
2.9 - else if no_thycontext guh then message2xmlTODO cI ("no thy-context for '" ^ guh ^ "'")
2.10 + then message2xml cI "thy-context not to calchead"
2.11 + else if ip = ([],Res) then message2xml cI "no thy-context at result"
2.12 + else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
2.13 else
2.14 ((let
2.15 val (ptp as (pt, pold), _) = get_calc cI
2.16 @@ -396,11 +396,11 @@
2.17 | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
2.18 (upd_calc cI ((pt,p), []);
2.19 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
2.20 - | ("end-of-calculation",_) => message2xmlTODO cI "end-of-calculation"
2.21 + | ("end-of-calculation",_) => message2xml cI "end-of-calculation"
2.22 | ("failure",_) => sysERROR2xml cI "failure"
2.23 | ("not-applicable",_) => (*the rule comes from anywhere..*)
2.24 (case applicable_in ip pt tac of
2.25 - Notappl e => message2xmlTODO cI ("'" ^ tac2str tac ^ "' not-applicable")
2.26 + Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
2.27 | Appl m =>
2.28 let
2.29 val ctxt = get_ctxt pt pold
2.30 @@ -659,8 +659,8 @@
2.31 at possible pos's there can be NO rewrite (returned as a context, too).*)
2.32 fun initContext (cI:calcID) Thy_ (pos as (p, p_):pos') =
2.33 ((if member op = [Pbl, Met] p_
2.34 - then message2xmlTODO cI "thy-context not to calchead"
2.35 - else if pos = ([], Res) then message2xmlTODO cI "no thy-context at result"
2.36 + then message2xml cI "thy-context not to calchead"
2.37 + else if pos = ([], Res) then message2xml cI "no thy-context at result"
2.38 else
2.39 let val cs as (ptp as (pt, _), _) = get_calc cI
2.40 in
2.41 @@ -672,7 +672,7 @@
2.42 in
2.43 if is_rewtac tac
2.44 then contextthyOK2xml cI (context_thy (pt, pos) tac)
2.45 - else message2xmlTODO cI ("no thy-context at tac '" ^ tac2str tac ^ "'")
2.46 + else message2xml cI ("no thy-context at tac '" ^ tac2str tac ^ "'")
2.47 end
2.48 else if is_curr_endof_calc pt pos
2.49 then
2.50 @@ -682,10 +682,10 @@
2.51 in
2.52 if is_rewtac tac
2.53 then contextthyOK2xml cI (context_thy ptp tac)
2.54 - else message2xmlTODO cI ("no thy-context at tac '" ^ tac2str tac ^ "'")
2.55 + else message2xml cI ("no thy-context at tac '" ^ tac2str tac ^ "'")
2.56 end
2.57 - | (msg, _) => message2xmlTODO cI msg
2.58 - else message2xmlTODO cI "no thy-context at this position"
2.59 + | (msg, _) => message2xml cI msg
2.60 + else message2xml cI "no thy-context at this position"
2.61 end)
2.62 handle _ => sysERROR2xml cI "error in kernel")
2.63
2.64 @@ -711,9 +711,9 @@
2.65 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
2.66 "thy_" =>
2.67 if member op = [Pbl,Met] p_
2.68 - then message2xmlTODO cI "thy-context not to calchead"
2.69 - else if pos = ([],Res) then message2xmlTODO cI "no thy-context at result"
2.70 - else if no_thycontext guh then message2xmlTODO cI ("no thy-context for '" ^ guh ^ "'")
2.71 + then message2xml cI "thy-context not to calchead"
2.72 + else if pos = ([],Res) then message2xml cI "no thy-context at result"
2.73 + else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
2.74 else
2.75 ((let
2.76 val (ptp as (pt,_),_) = get_calc cI
2.77 @@ -804,7 +804,7 @@
2.78 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
2.79 | (str,_) => autocalculateERROR2xml cI "failure"
2.80 end
2.81 - | (msg, _) => message2xmlTODO cI msg
2.82 + | (msg, _) => message2xml cI msg
2.83 end
2.84
2.85 (*------------------------------------------------------------------*)
3.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Sun May 31 10:31:53 2015 +0200
3.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Sun May 31 10:37:31 2015 +0200
3.3 @@ -325,7 +325,7 @@
3.4 " <STRING> "^e^" </STRING>\n" ^
3.5 "</MESSAGE>\n" ^
3.6 "@@@@@end@@@@@");
3.7 -fun message2xmlTODO (calcid : calcID) e =
3.8 +fun message2xml (calcid : calcID) e =
3.9 XML.Elem (("MESSAGE", []), [
3.10 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.11 XML.Elem (("STRING", []), [XML.Text e])])
4.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Sun May 31 10:31:53 2015 +0200
4.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Sun May 31 10:37:31 2015 +0200
4.3 @@ -13,10 +13,4 @@
4.4 ML_file "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml"
4.5 ML_file "~~/src/Tools/isac/xmlsrc/interface-xml.sml"
4.6
4.7 -ML {*
4.8 -*} ML {*
4.9 -*} ML {*
4.10 -*} ML {*
4.11 -*}
4.12 -
4.13 end
4.14 \ No newline at end of file