eliminate "handle _ => ..." by \<^try>CARTOUCHE in Libisabelle/interface.sml for tests
note: the tests do not involve Isabelle/PIDE, thus this changeset has probably no effect.
1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Sat Apr 24 15:59:54 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Sun Apr 25 12:03:49 2021 +0200
1.3 @@ -69,18 +69,22 @@
1.4 all others are just calculated on the fly
1.5 TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
1.6 fun Iterator cI = (*returned ID unnecessary after WN.0411*)
1.7 - (adduserOK2xml cI (add_user cI ))
1.8 - handle _ => sysERROR2xml cI "error in kernel 1";
1.9 + case \<^try>\<open> (adduserOK2xml cI (add_user cI ))\<close> of
1.10 + SOME xml => xml
1.11 + | NONE => sysERROR2xml cI "error in kernel 1";
1.12 fun IteratorTEST cI = add_user cI;
1.13
1.14 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
1.15 compare "fun CalcTreeTEST" which does NOT decode.*)
1.16 fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
1.17 - ((let
1.18 - val cs = Step_Specify.nxt_specify_init_calc (fmz, sp)
1.19 - val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
1.20 - in calctreeOK2xml cI end)
1.21 - handle _ => sysERROR2xml 0 "error in kernel 2")
1.22 + (case \<^try>\<open>
1.23 + let
1.24 + val cs = Step_Specify.nxt_specify_init_calc (fmz, sp)
1.25 + val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
1.26 + in calctreeOK2xml cI end
1.27 + \<close> of
1.28 + SOME xml => xml
1.29 + | NONE => sysERROR2xml 0 "error in kernel 2")
1.30 | CalcTree [] = error "CalcTree: called with []"
1.31
1.32 fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (del_calc cI);
1.33 @@ -136,17 +140,19 @@
1.34 end;
1.35
1.36 fun fetchProposedTactic cI =
1.37 - (case Step.do_next (get_pos cI 1) (get_calc cI) of
1.38 - ("ok", (tacis, _, _)) =>
1.39 - let
1.40 - val _= upd_tacis cI tacis
1.41 - val (tac, _, _) = last_elem tacis
1.42 - in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
1.43 - | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
1.44 - | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
1.45 - | ("end-of-calculation", _) =>
1.46 - fetchproposedtacticERROR2xml cI "end-of-calculation")
1.47 - handle _ => sysERROR2xml cI "error in kernel 3";
1.48 + case \<^try>\<open>
1.49 + (case Step.do_next (get_pos cI 1) (get_calc cI) of
1.50 + ("ok", (tacis, _, _)) =>
1.51 + let
1.52 + val _ = upd_tacis cI tacis
1.53 + val (tac, _, _) = last_elem tacis
1.54 + in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
1.55 + | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
1.56 + | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
1.57 + | ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation")
1.58 + \<close> of
1.59 + SOME xml => xml
1.60 + | NONE => sysERROR2xml cI "error in kernel 3";
1.61
1.62 fun autoCalculate cI auto = (*Future.fork
1.63 (fn () => (( *)let
1.64 @@ -167,15 +173,18 @@
1.65 handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);
1.66
1.67 fun getTactic cI (p:pos') =
1.68 - (let
1.69 - val ((pt, _), _) = get_calc cI
1.70 - val (_, tac, _) = ME_Misc.pt_extract (pt, p)
1.71 - in
1.72 - case tac of
1.73 - SOME ta => gettacticOK2xml cI ta
1.74 - | NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)
1.75 - end)
1.76 - handle _ => sysERROR2xml cI "syserror in getTactic";
1.77 + case \<^try>\<open>
1.78 + let
1.79 + val ((pt, _), _) = get_calc cI
1.80 + val (_, tac, _) = ME_Misc.pt_extract (pt, p)
1.81 + in
1.82 + case tac of
1.83 + SOME ta => gettacticOK2xml cI ta
1.84 + | NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)
1.85 + end
1.86 + \<close> of
1.87 + SOME xml => xml
1.88 + | NONE => sysERROR2xml cI "syserror in getTactic";
1.89
1.90 (* Fetch tactics to be applied to a particular step.
1.91 Requirements are not yet implemented, see ICalcIterator#fetchApplicableTactics"
1.92 @@ -185,53 +194,68 @@
1.93 LItool.specific_from_prog waits to be used here
1.94 *)
1.95 fun fetchApplicableTactics cI (_(*scope*): int) (p : pos') =
1.96 - (let val ((pt, _), _) = get_calc cI
1.97 - in (applicabletacticsOK cI (Fetch_Tacs.from_prog pt p))
1.98 - handle PTREE str => sysERROR2xml cI str
1.99 - end)
1.100 - handle _ => sysERROR2xml cI "error in kernel 5";
1.101 + case \<^try>\<open>
1.102 + let val ((pt, _), _) = get_calc cI
1.103 + in (applicabletacticsOK cI (Fetch_Tacs.from_prog pt p))
1.104 + handle PTREE str => sysERROR2xml cI str
1.105 + end
1.106 + \<close> of
1.107 + SOME xml => xml
1.108 + | NONE => sysERROR2xml cI "error in kernel 5";
1.109
1.110 fun getAssumptions cI (p:pos') =
1.111 - (let
1.112 - val ((pt, _), _) = get_calc cI
1.113 - val (_, _, asms) = ME_Misc.pt_extract (pt, p)
1.114 - in getasmsOK2xml cI asms end)
1.115 - handle _ => sysERROR2xml cI "syserror in getAssumptions"
1.116 + case \<^try>\<open>
1.117 + let
1.118 + val ((pt, _), _) = get_calc cI
1.119 + val (_, _, asms) = ME_Misc.pt_extract (pt, p)
1.120 + in getasmsOK2xml cI asms end
1.121 + \<close> of
1.122 + SOME xml => xml
1.123 + | NONE => sysERROR2xml cI "syserror in getAssumptions"
1.124
1.125 (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
1.126 fun getAccumulatedAsms cI (p:pos') =
1.127 - (let
1.128 - val ((pt, _), _) = get_calc cI
1.129 - val ass = Ctree.get_assumptions pt p
1.130 - in getasmsOK2xml cI ass end)
1.131 - handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"
1.132 + case \<^try>\<open>
1.133 + let
1.134 + val ((pt, _), _) = get_calc cI
1.135 + val ass = Ctree.get_assumptions pt p
1.136 + in getasmsOK2xml cI ass end
1.137 + \<close> of
1.138 + SOME xml => xml
1.139 + | NONE => sysERROR2xml cI "syserror in getAccumulatedAsms"
1.140
1.141 fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
1.142 - (let
1.143 - val ((pt, _), _) = get_calc cI
1.144 - val (form, _, _) = ME_Misc.pt_extract (pt, p)
1.145 - in refformulaOK2xml cI p form end)
1.146 - handle _ => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)
1.147 + case \<^try>\<open>
1.148 + let
1.149 + val ((pt, _), _) = get_calc cI
1.150 + val (form, _, _) = ME_Misc.pt_extract (pt, p)
1.151 + in refformulaOK2xml cI p form end
1.152 + \<close> of
1.153 + SOME xml => xml
1.154 + | NONE => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)
1.155
1.156 (* get formulae "from" "to" w.r.t. ordering in Position#compareTo(Position p);
1.157 "level" is adjusted such that an "interval" of formulae is returned;
1.158 "from" "to" are designed for use by iterators of calcChangedEvent,
1.159 thus "from" is the last unchanged position *)
1.160 fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =
1.161 - ((let
1.162 + (case \<^try>\<open>
1.163 + let
1.164 val ((pt,_),_) = get_calc cI
1.165 val headline =
1.166 case ME_Misc.pt_extract (pt, to) of
1.167 (ModSpec (_, _, headline, _, _, _), _, _) => headline
1.168 | _ => raise ERROR "getFormulaeFromTo: uncovered case of ME_Misc.pt_extract"
1.169 - in getintervalOK cI [(to, headline, NONE)] end)
1.170 - handle _ => sysERROR2xml cI "error in kernel 7")
1.171 + in getintervalOK cI [(to, headline, NONE)] end
1.172 + \<close> of
1.173 + SOME xml => xml
1.174 + | NONE => sysERROR2xml cI "error in kernel 7")
1.175 | getFormulaeFromTo cI ([], Pbl) ([], Met) _ false =
1.176 getFormulaeFromTo cI ([], Pbl) ([], Pbl) (~00000) false
1.177 (* ^^^ separated cases, because "from" is _before_ the first elements to be returned*)
1.178 | getFormulaeFromTo cI from to level false =
1.179 - (if from = to
1.180 - then sysERROR2xml cI "getFormulaeFromTo: From = To"
1.181 + (case \<^try>\<open>
1.182 + if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
1.183 else
1.184 (case from of
1.185 ([], Res) => sysERROR2xml cI ("getFormulaeFromTo does: moveDown " ^
1.186 @@ -243,182 +267,135 @@
1.187 fun max (a,b) = if a < b then b else a
1.188 val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
1.189 in getintervalOK cI (ME_Misc.get_interval f to lev pt) end)
1.190 - handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
1.191 - | getFormulaeFromTo cI from to level true =
1.192 + \<close> of
1.193 + SOME xml => xml
1.194 + | NONE => sysERROR2xml cI "error in getFormulaeFromTo")
1.195 + | getFormulaeFromTo cI _ _ _ true =
1.196 sysERROR2xml cI ("getFormulaeFromTo impl.for formulae only, " ^
1.197 "i.e. last arg only impl. for false, _NOT_ true");
1.198
1.199 fun interSteps cI ip =
1.200 - (let val ((pt, p), tacis) = get_calc cI
1.201 - in
1.202 - if (not o is_interpos) ip
1.203 - then interStepsERROR cI ("only formulae with position (_,Res) " ^
1.204 - "may have intermediate steps above them")
1.205 - else
1.206 - let val ip' = lev_pred' pt ip
1.207 - in case Detail_Step.go pt ip of
1.208 - ("detailrls", pt, lastpos) =>
1.209 - (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
1.210 - | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
1.211 - | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
1.212 - end
1.213 - end)
1.214 - handle _ => sysERROR2xml cI "error in kernel 8";
1.215 + case \<^try>\<open>
1.216 + let val ((pt, p), tacis) = get_calc cI
1.217 + in
1.218 + if (not o is_interpos) ip
1.219 + then interStepsERROR cI ("only formulae with position (_,Res) " ^
1.220 + "may have intermediate steps above them")
1.221 + else
1.222 + let val ip' = lev_pred' pt ip
1.223 + in case Detail_Step.go pt ip of
1.224 + ("detailrls", pt, lastpos) =>
1.225 + (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
1.226 + | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
1.227 + | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
1.228 + end
1.229 + end
1.230 + \<close> of
1.231 + SOME xml => xml
1.232 + | NONE => sysERROR2xml cI "error in kernel 8";
1.233
1.234 fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Spec.icalhd) =
1.235 - (let
1.236 - val ((pt,_),_) = get_calc cI
1.237 - val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd
1.238 - in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)
1.239 - handle _ => sysERROR2xml cI "error in kernel 9";
1.240 + case \<^try>\<open>
1.241 + let
1.242 + val ((pt,_),_) = get_calc cI
1.243 + val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd
1.244 + in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end
1.245 + \<close> of
1.246 + SOME xml => xml
1.247 + | NONE => sysERROR2xml cI "error in kernel 9";
1.248
1.249 (* at the activeFormula set the Model, the Guard and the Specification to empty
1.250 and return a CalcHead; the 'origin' remains (for reconstructing all that) *)
1.251 fun resetCalcHead cI =
1.252 - (let
1.253 - val (ptp,_) = get_calc cI
1.254 - val ptp = SpecificationC.reset ptp
1.255 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end)
1.256 - handle _ => sysERROR2xml cI "error in kernel 10";
1.257 + case \<^try>\<open>
1.258 + let
1.259 + val (ptp,_) = get_calc cI
1.260 + val ptp = SpecificationC.reset ptp
1.261 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
1.262 + \<close> of
1.263 + SOME xml => xml
1.264 + | NONE => sysERROR2xml cI "error in kernel 10";
1.265
1.266 (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
1.267 the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
1.268 fun modelProblem cI =
1.269 - (let val (ptp, _) = get_calc cI
1.270 - val ptp = SpecificationC.reset ptp
1.271 - val (_, (_, _, ptp)) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
1.272 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end)
1.273 - handle _ => sysERROR2xml cI "error in kernel 11";
1.274 -
1.275 -(** )
1.276 -(* set the UContext determined on a knowledgebrowser to the current calc
1.277 - WN0825: not implemented in isac-java.
1.278 - Recalling the state of development after summer-term 2006 (Robert Koenishofer et.al.):
1.279 - Main success was showing UContext from Worksheet to the Example/MethodC/Problem/TheoryBrowser,
1.280 - while the buttons on these browsers <To Worksheet> <Try Refine> have no
1.281 - code in isac-java (and only partial, untested code in isabisac).
1.282 -*)
1.283 -fun setContext cI (ip as (_,p_)) guh =
1.284 - case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.285 - "thy_" =>
1.286 - if member op = [Pbl, Met] p_
1.287 - then message2xml cI "thy-context not to calchead"
1.288 - else if ip = ([], Res) then message2xml cI "no thy-context at result"
1.289 - else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
1.290 - else
1.291 - ((let
1.292 - val (ptp as (pt, pold), _) = get_calc cI
1.293 - val is = get_istate_LI pt ip
1.294 - val subs = Thy_Present.subs_from is "dummy" guh
1.295 - val tac = Thy_Present.guh2rewtac guh subs
1.296 - in
1.297 - case Step.by_tactic tac (pt, ip) of (*='fun setNextTactic'+step*)
1.298 - ("ok", (tacis, c, ptp as (_, p))) =>
1.299 - (upd_calc cI ((pt, p), []);
1.300 - autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.301 - | ("unsafe-ok", (tacis, c, ptp as (_ ,p))) =>
1.302 - (upd_calc cI ((pt, p), []);
1.303 - autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
1.304 - | ("end-of-calculation", _) => message2xml cI "end-of-calculation"
1.305 - | ("failure", _) => sysERROR2xml cI "failure"
1.306 - | ("not-applicable", _) => (*the rule comes from anywhere..*)
1.307 - (case Step.check tac (pt, ip) of
1.308 - Applicable.No e => message2xml cI ("'" ^ Tactic.input_to_string tac ^ "' not-applicable")
1.309 - | Applicable.Yes m =>
1.310 - let
1.311 - val ctxt = get_ctxt pt pold
1.312 - val (p, c, _, pt) =
1.313 - Step.add m (Istate.Uistate, ctxt) (pt, ip)
1.314 - in upd_calc cI ((pt, p), []);
1.315 - autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
1.316 - end)
1.317 - end
1.318 - ) handle _ => sysERROR2xml cI "setContext: thy_ ???")
1.319 - | "pbl_" =>
1.320 - ((let
1.321 - val pI = Ptool.guh2kestoreID guh
1.322 - val ((pt, _), _) = get_calc cI
1.323 - in
1.324 - if member op = [Pbl, Met] p_
1.325 - then
1.326 - let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
1.327 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.328 - else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"
1.329 - end
1.330 - ) handle _ => sysERROR2xml cI "setContext: pbl_ ???")
1.331 - | "met_" =>
1.332 - ((let
1.333 - val mI = Ptool.guh2kestoreID guh
1.334 - val ((pt, _), _) = get_calc cI
1.335 - in
1.336 - if member op = [Pbl, Met] p_
1.337 - then
1.338 - let
1.339 - val (pt, chd) = Math_Engine.set_method mI (pt, ip)
1.340 - in
1.341 - (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd)
1.342 - end
1.343 - else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
1.344 - end
1.345 - ) handle _ => sysERROR2xml cI "setContext: met_ ???")
1.346 -( **)
1.347 + case \<^try>\<open>
1.348 + let val (ptp, _) = get_calc cI
1.349 + val ptp = SpecificationC.reset ptp
1.350 + val (_, (_, _, ptp)) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
1.351 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
1.352 + \<close> of
1.353 + SOME xml => xml
1.354 + | NONE => sysERROR2xml cI "error in kernel 11";
1.355
1.356
1.357 (* specify the MethodC at the activeFormula and return a CalcHead containing the Guard.
1.358 WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
1.359 fun setMethod cI mI =
1.360 - (let
1.361 - val ((pt, _), _) = get_calc cI
1.362 - val ip as (_, p_) = get_pos cI 1
1.363 - in
1.364 - if member op = [Pbl,Met] p_
1.365 - then
1.366 - let val (pt, chd) = Math_Engine.set_method mI (pt, ip)
1.367 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.368 - else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
1.369 - end
1.370 - ) handle _ => sysERROR2xml cI "error in kernel 12";
1.371 + case \<^try>\<open>
1.372 + let
1.373 + val ((pt, _), _) = get_calc cI
1.374 + val ip as (_, p_) = get_pos cI 1
1.375 + in
1.376 + if member op = [Pbl,Met] p_
1.377 + then
1.378 + let val (pt, chd) = Math_Engine.set_method mI (pt, ip)
1.379 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.380 + else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
1.381 + end
1.382 + \<close> of
1.383 + SOME xml => xml
1.384 + | NONE => sysERROR2xml cI "error in kernel 12";
1.385
1.386 (* specify the Problem at the activeFormula and return a CalcHead containing the Model;
1.387 special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Problem" *)
1.388 fun setProblem cI pI =
1.389 - (let
1.390 - val ((pt, _), _) = get_calc cI
1.391 - val ip as (_, p_) = get_pos cI 1
1.392 - in
1.393 - if member op = [Pbl,Met] p_
1.394 - then
1.395 - let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
1.396 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.397 - else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.398 - end
1.399 - ) handle _ => sysERROR2xml cI "error in kernel 13";
1.400 + case \<^try>\<open>
1.401 + let
1.402 + val ((pt, _), _) = get_calc cI
1.403 + val ip as (_, p_) = get_pos cI 1
1.404 + in
1.405 + if member op = [Pbl,Met] p_
1.406 + then
1.407 + let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
1.408 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.409 + else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.410 + end
1.411 + \<close> of
1.412 + SOME xml => xml
1.413 + | NONE => sysERROR2xml cI "error in kernel 13";
1.414
1.415 (* specify the Theory at the activeFormula and return a CalcHead;
1.416 special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
1.417 fun setTheory cI tI =
1.418 - (let
1.419 - val ((pt, _), _) = get_calc cI
1.420 - val ip as (_, p_) = get_pos cI 1
1.421 - in
1.422 - if member op = [Pbl,Met] p_
1.423 - then
1.424 - let val (pt, chd) = Math_Engine.set_theory tI (pt, ip)
1.425 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.426 - else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.427 - end
1.428 - ) handle _ => sysERROR2xml cI "error in kernel 14";
1.429 + case \<^try>\<open>
1.430 + let
1.431 + val ((pt, _), _) = get_calc cI
1.432 + val ip as (_, p_) = get_pos cI 1
1.433 + in
1.434 + if member op = [Pbl,Met] p_
1.435 + then
1.436 + let val (pt, chd) = Math_Engine.set_theory tI (pt, ip)
1.437 + in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
1.438 + else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
1.439 + end
1.440 + \<close> of
1.441 + SOME xml => xml
1.442 + | NONE => sysERROR2xml cI "error in kernel 14";
1.443
1.444 (* refinement for the parent-problem of the position,
1.445 Not used in isac-java (see comment WN0825 for setContext) but tryrefine is used within isabisac *)
1.446 fun refineProblem cI (p, p_) guh =
1.447 - (let
1.448 - val pblID = Ptool.guh2kestoreID guh
1.449 - val ((pt,_),_) = get_calc cI
1.450 - val pp = par_pblobj pt p
1.451 - val chd = Math_Engine.tryrefine pblID pt (pp, p_)
1.452 - in contextpblOK2xml cI chd end)
1.453 - handle _ => sysERROR2xml cI "error in kernel 16";
1.454 + case \<^try>\<open>
1.455 + let
1.456 + val pblID = Ptool.guh2kestoreID guh
1.457 + val ((pt,_),_) = get_calc cI
1.458 + val pp = par_pblobj pt p
1.459 + val chd = Math_Engine.tryrefine pblID pt (pp, p_)
1.460 + in contextpblOK2xml cI chd end
1.461 + \<close> of
1.462 + SOME xml => xml
1.463 + | NONE => sysERROR2xml cI "error in kernel 16";
1.464
1.465 (* append a formula to the calculation *)
1.466 fun appendFormula' cI (ifo: TermC.as_string) =
1.467 @@ -444,21 +421,24 @@
1.468
1.469 (* replace a formula with_in_ a calculation; this applies for initial CAS-commands, too *)
1.470 fun replaceFormula cI ifo =
1.471 - (let
1.472 - val ((pt, _), _) = get_calc cI
1.473 - val p = get_pos cI 1
1.474 - in
1.475 - case Step_Solve.by_term (pt, p) (encode ifo) of
1.476 - ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
1.477 - let
1.478 - val unc = if null (fst p) then p else move_up [] pt p
1.479 - val _ = upd_calc cI (ptp', [])
1.480 - val _ = upd_ipos cI 1 p'
1.481 - in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end
1.482 - | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"
1.483 - | (msg, _) => replaceformulaERROR2xml cI msg
1.484 - end)
1.485 - handle _ => sysERROR2xml cI "error in kernel 18";
1.486 + case \<^try>\<open>
1.487 + let
1.488 + val ((pt, _), _) = get_calc cI
1.489 + val p = get_pos cI 1
1.490 + in
1.491 + case Step_Solve.by_term (pt, p) (encode ifo) of
1.492 + ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
1.493 + let
1.494 + val unc = if null (fst p) then p else move_up [] pt p
1.495 + val _ = upd_calc cI (ptp', [])
1.496 + val _ = upd_ipos cI 1 p'
1.497 + in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end
1.498 + | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"
1.499 + | (msg, _) => replaceformulaERROR2xml cI msg
1.500 + end
1.501 + \<close> of
1.502 + SOME xml => xml
1.503 + | NONE => sysERROR2xml cI "error in kernel 18";
1.504
1.505 (*** CalcIterator
1.506 moveActive*: set the pos' of the active formula stored with the calctree
1.507 @@ -467,176 +447,135 @@
1.508 ***)
1.509
1.510 fun moveActiveRoot cI =
1.511 - (let val _ = upd_ipos cI 1 ([], Pbl)
1.512 - in iteratorOK2xml cI ([], Pbl) end)
1.513 - handle _ => sysERROR2xml cI "error in kernel 19"
1.514 + case \<^try>\<open>
1.515 + let val _ = upd_ipos cI 1 ([], Pbl)
1.516 + in iteratorOK2xml cI ([], Pbl) end
1.517 + \<close> of
1.518 + SOME xml => xml
1.519 + | NONE => sysERROR2xml cI "error in kernel 19"
1.520 fun moveRoot cI =
1.521 - (iteratorOK2xml cI ([], Pbl))
1.522 - handle _ => sysERROR2xml cI "";
1.523 + case \<^try>\<open>
1.524 + iteratorOK2xml cI ([], Pbl)
1.525 + \<close> of
1.526 + SOME xml => xml
1.527 + | NONE => sysERROR2xml cI "";
1.528 fun moveActiveRootTEST cI =
1.529 - (let val _ = upd_ipos cI 1 ([], Pbl)
1.530 - in iteratorOK2xml cI ([], Pbl) end)
1.531 - handle _ => sysERROR2xml cI "error in kernel 20"
1.532 + case \<^try>\<open>
1.533 + let val _ = upd_ipos cI 1 ([], Pbl)
1.534 + in iteratorOK2xml cI ([], Pbl) end
1.535 + \<close> of
1.536 + SOME xml => xml
1.537 + | NONE => sysERROR2xml cI "error in kernel 20"
1.538
1.539 fun moveActiveDown cI =
1.540 - ((let
1.541 - val ((pt, _), _) = get_calc cI
1.542 - val ip' = move_dn [] pt (get_pos cI 1)
1.543 - val _ = upd_ipos cI 1 ip'
1.544 - in iteratorOK2xml cI ip' end)
1.545 - handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 21"
1.546 + case \<^try>\<open>
1.547 + (let
1.548 + val ((pt, _), _) = get_calc cI
1.549 + val ip' = move_dn [] pt (get_pos cI 1)
1.550 + val _ = upd_ipos cI 1 ip'
1.551 + in iteratorOK2xml cI ip' end)
1.552 + handle (PTREE _) => iteratorERROR2xml cI
1.553 + \<close> of
1.554 + SOME xml => xml
1.555 + | NONE => sysERROR2xml cI "error in kernel 21"
1.556 fun moveDown cI p =
1.557 - ((let
1.558 - val ((pt, _), _) = get_calc cI
1.559 - val ip' = move_dn [] pt p
1.560 - in iteratorOK2xml cI ip' end)
1.561 - handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 22"
1.562 + case \<^try>\<open>
1.563 + (let
1.564 + val ((pt, _), _) = get_calc cI
1.565 + val ip' = move_dn [] pt p
1.566 + in iteratorOK2xml cI ip' end)
1.567 + handle (PTREE _) => iteratorERROR2xml cI
1.568 + \<close> of
1.569 + SOME xml => xml
1.570 + | NONE => sysERROR2xml cI "error in kernel 22"
1.571
1.572 fun moveActiveLevelDown cI =
1.573 - ((let
1.574 - val ((pt, _) ,_) = get_calc cI
1.575 - val ip' = movelevel_dn [] pt (get_pos cI 1)
1.576 - val _ = upd_ipos cI 1 ip'
1.577 - in iteratorOK2xml cI ip' end)
1.578 - handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 23"
1.579 + case \<^try>\<open>
1.580 + (let
1.581 + val ((pt, _) ,_) = get_calc cI
1.582 + val ip' = movelevel_dn [] pt (get_pos cI 1)
1.583 + val _ = upd_ipos cI 1 ip'
1.584 + in iteratorOK2xml cI ip' end)
1.585 + handle (PTREE _) => iteratorERROR2xml cI
1.586 + \<close> of
1.587 + SOME xml => xml
1.588 + | NONE => sysERROR2xml cI "error in kernel 23"
1.589 fun moveLevelDown cI p =
1.590 - ((let
1.591 - val ((pt, _), _) = get_calc cI
1.592 - val ip' = movelevel_dn [] pt p
1.593 - in iteratorOK2xml cI ip' end)
1.594 - handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 24"
1.595 + case \<^try>\<open>
1.596 + (let
1.597 + val ((pt, _), _) = get_calc cI
1.598 + val ip' = movelevel_dn [] pt p
1.599 + in iteratorOK2xml cI ip' end)
1.600 + handle (PTREE _) => iteratorERROR2xml cI
1.601 + \<close> of
1.602 + SOME xml => xml
1.603 + | NONE => sysERROR2xml cI "error in kernel 24"
1.604
1.605 fun moveActiveUp cI =
1.606 - ((let
1.607 - val ((pt, _), _) = get_calc cI
1.608 - val ip' = move_up [] pt (get_pos cI 1)
1.609 - val _ = upd_ipos cI 1 ip'
1.610 - in iteratorOK2xml cI ip' end)
1.611 - handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 25"
1.612 + case \<^try>\<open>
1.613 + (let
1.614 + val ((pt, _), _) = get_calc cI
1.615 + val ip' = move_up [] pt (get_pos cI 1)
1.616 + val _ = upd_ipos cI 1 ip'
1.617 + in iteratorOK2xml cI ip' end)
1.618 + handle PTREE _ => iteratorERROR2xml cI
1.619 + \<close> of
1.620 + SOME xml => xml
1.621 + | NONE => sysERROR2xml cI "error in kernel 25"
1.622 fun moveUp cI p =
1.623 - ((let
1.624 - val ((pt, _), _) = get_calc cI
1.625 - val ip' = move_up [] pt p
1.626 - in iteratorOK2xml cI ip' end)
1.627 - handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 26"
1.628 + case \<^try>\<open>
1.629 + (let
1.630 + val ((pt, _), _) = get_calc cI
1.631 + val ip' = move_up [] pt p
1.632 + in iteratorOK2xml cI ip' end)
1.633 + handle PTREE _ => iteratorERROR2xml cI
1.634 + \<close> of
1.635 + SOME xml => xml
1.636 + | NONE => sysERROR2xml cI "error in kernel 26"
1.637
1.638 fun moveActiveLevelUp cI =
1.639 - ((let
1.640 - val ((pt, _), _) = get_calc cI
1.641 - val ip' = movelevel_up [] pt (get_pos cI 1)
1.642 - val _ = upd_ipos cI 1 ip'
1.643 - in iteratorOK2xml cI ip' end)
1.644 - handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 27"
1.645 + case \<^try>\<open>
1.646 + (let
1.647 + val ((pt, _), _) = get_calc cI
1.648 + val ip' = movelevel_up [] pt (get_pos cI 1)
1.649 + val _ = upd_ipos cI 1 ip'
1.650 + in iteratorOK2xml cI ip' end)
1.651 + handle PTREE _ => iteratorERROR2xml cI
1.652 + \<close> of
1.653 + SOME xml => xml
1.654 + | NONE => sysERROR2xml cI "error in kernel 27"
1.655 fun moveLevelUp cI p =
1.656 - ((let
1.657 - val ((pt, _), _) = get_calc cI
1.658 - val ip' = movelevel_up [] pt p
1.659 - in iteratorOK2xml cI ip' end)
1.660 - handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 28"
1.661 + case \<^try>\<open>
1.662 + (let
1.663 + val ((pt, _), _) = get_calc cI
1.664 + val ip' = movelevel_up [] pt p
1.665 + in iteratorOK2xml cI ip' end)
1.666 + handle PTREE _ => iteratorERROR2xml cI
1.667 + \<close> of
1.668 + SOME xml => xml
1.669 + | NONE => sysERROR2xml cI "error in kernel 28"
1.670
1.671 fun moveActiveCalcHead cI =
1.672 - ((let
1.673 + case \<^try>\<open>
1.674 + (let
1.675 val ((pt, _), _) = get_calc cI
1.676 val ip' = movecalchd_up pt (get_pos cI 1)
1.677 val _ = upd_ipos cI 1 ip'
1.678 in iteratorOK2xml cI ip' end)
1.679 - handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 29"
1.680 + handle PTREE _ => iteratorERROR2xml cI
1.681 + \<close> of
1.682 + SOME xml => xml
1.683 + | NONE => sysERROR2xml cI "error in kernel 29"
1.684 fun moveCalcHead cI p =
1.685 - ((let
1.686 - val ((pt, _), _) = get_calc cI
1.687 - val ip' = movecalchd_up pt p
1.688 - in iteratorOK2xml cI ip' end)
1.689 - handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 30"
1.690 -
1.691 -(** )
1.692 -(*.initContext Thy_ is conceptually impossible at [Pbl,Met]
1.693 - and at positions with Check_Postcond and End_Trans;
1.694 - at possible pos's there can be NO rewrite (returned as a context, too).*)
1.695 -fun initContext cI Ptool.Thy_ (pos as (p, p_):pos') =
1.696 - ((if member op = [Pos.Pbl, Pos.Met] p_
1.697 - then message2xml cI "thy-context not to calchead"
1.698 - else if pos = ([], Res) then message2xml cI "no thy-context at result"
1.699 - else
1.700 - let val cs as (ptp as (pt, _), _) = get_calc cI
1.701 - in
1.702 - if exist_lev_on' pt pos
1.703 - then
1.704 - let
1.705 - val pos' = lev_on' pt pos
1.706 - val tac = Thy_Present.get_tac_checked pt pos'
1.707 - in
1.708 - if Tactic.is_rewtac tac
1.709 - then contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac)
1.710 - else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
1.711 - end
1.712 - else if is_curr_endof_calc pt pos
1.713 - then
1.714 - case Step.do_next pos cs of
1.715 - ("ok", (tacis, _, (pt, _))) =>
1.716 - let val tac = fst3 (last_elem tacis)
1.717 - in
1.718 - if Tactic.is_rewtac tac
1.719 - then contextthyOK2xml cI (Thy_Present.context_thy ptp tac)
1.720 - else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
1.721 - end
1.722 - | (msg, _) => message2xml cI msg
1.723 - else message2xml cI "no thy-context at this position"
1.724 - end)
1.725 - handle _ => sysERROR2xml cI "error in kernel 31")
1.726 - | initContext cI Ptool.Pbl_ (p, p_) =
1.727 - ((let
1.728 + case \<^try>\<open>
1.729 + (let
1.730 val ((pt, _), _) = get_calc cI
1.731 - val pp = par_pblobj pt p
1.732 - val chd = Math_Engine.initcontext_pbl pt (pp,p_)
1.733 - in contextpblOK2xml cI chd end)
1.734 - handle _ => sysERROR2xml cI "error in kernel 32")
1.735 - | initContext cI Ptool.Met_ (p, p_) =
1.736 - ((let
1.737 - val ((pt,_),_) = get_calc cI
1.738 - val pp = par_pblobj pt p
1.739 - val chd = Math_Engine.initcontext_met pt (pp,p_)
1.740 - in contextmetOK2xml cI chd end)
1.741 - handle _ => sysERROR2xml cI "error in kernel 33");
1.742 -
1.743 -(* match a theorem, a ruleset (etc., selected in the knowledge-browser)
1.744 - with the formula in the focus on the worksheet;
1.745 - string contains the thy, thus it is unique as thmID, rlsID for this thy;
1.746 - take the substitution from the istate of the formula *)
1.747 -fun checkContext cI (pos as (p, p_)) guh =
1.748 - case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.749 - "thy_" =>
1.750 - if member op = [Pbl, Met] p_
1.751 - then message2xml cI "thy-context not to calchead"
1.752 - else if pos = ([],Res) then message2xml cI "no thy-context at result"
1.753 - else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
1.754 - else
1.755 - ((let
1.756 - val ((pt,_),_) = get_calc cI
1.757 - val is = get_istate_LI pt pos
1.758 - val subs = Thy_Present.subs_from is "dummy" guh
1.759 - val tac = Thy_Present.guh2rewtac guh subs
1.760 - in contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac) end
1.761 - ) handle _ => sysERROR2xml cI "error in kernel 34")
1.762 - (*.match the model of a problem at pos p
1.763 - with the model-pattern of the problem with pblID.*)
1.764 - | "pbl_" =>
1.765 - ((let
1.766 - val ((pt, _), _) = get_calc cI
1.767 - val pp = par_pblobj pt p
1.768 - val keID = Ptool.guh2kestoreID guh
1.769 - val chd = Math_Engine.context_pbl keID pt pp
1.770 - in contextpblOK2xml cI chd end
1.771 - ) handle _ => sysERROR2xml cI "error in kernel 35")
1.772 - | "met_" =>
1.773 - ((let
1.774 - val ((pt, _), _) = get_calc cI
1.775 - val pp = par_pblobj pt p
1.776 - val keID = Ptool.guh2kestoreID guh
1.777 - val chd = Math_Engine.context_met keID pt pp
1.778 - in contextmetOK2xml cI chd end
1.779 - ) handle _ => sysERROR2xml cI "error in kernel 36")
1.780 - | str => sysERROR2xml cI ("checkContext: str = " ^ str)
1.781 -( **)
1.782 + val ip' = movecalchd_up pt p
1.783 + in iteratorOK2xml cI ip' end)
1.784 + handle PTREE _ => iteratorERROR2xml cI
1.785 + \<close> of
1.786 + SOME xml => xml
1.787 + | NONE => sysERROR2xml cI "error in kernel 30"
1.788
1.789 (*
1.790 for an Error_Pattern.id find "(fill_in_id * fill_in) list"