wneuper/isa: comparison src/Tools/isac/BridgeLibisabelle/interface.sml

equal deleted inserted replaced

-:5765bd0f7055
+:c0a775618258
 as long as many tests imitate interaction via libisabelle.
 *)
 signature KERNEL =
 sig
-val appendFormula : calcID -> TermC.as_string -> XML.tree (*unit future*)
+val appendFormula : States.calcID -> TermC.as_string -> XML.tree (*unit future*)
-val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
+val autoCalculate : States.calcID -> Solve.auto -> XML.tree (*unit future*)
-val applyTactic : calcID -> Pos.pos' -> Tactic.input -> XML.tree
+val applyTactic : States.calcID -> Pos.pos' -> Tactic.input -> XML.tree
 val CalcTree : Formalise.T list -> XML.tree
-val DEconstrCalcTree : calcID -> XML.tree
+val DEconstrCalcTree : States.calcID -> XML.tree
-val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree
+val fetchApplicableTactics : States.calcID -> int -> Pos.pos' -> XML.tree
-val fetchProposedTactic : calcID -> XML.tree
+val fetchProposedTactic : States.calcID -> XML.tree
-val findFillpatterns : calcID -> Error_Pattern_Def.id -> XML.tree
+val findFillpatterns : States.calcID -> Error_Pattern_Def.id -> XML.tree
-val getAccumulatedAsms : calcID -> Pos.pos' -> XML.tree
+val getAccumulatedAsms : States.calcID -> Pos.pos' -> XML.tree
-val getActiveFormula : calcID -> XML.tree
+val getActiveFormula : States.calcID -> XML.tree
-val getAssumptions : calcID -> Pos.pos' -> XML.tree
+val getAssumptions : States.calcID -> Pos.pos' -> XML.tree
-val getFormulaeFromTo : calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
+val getFormulaeFromTo : States.calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
-val getTactic : calcID -> Pos.pos' -> XML.tree
+val getTactic : States.calcID -> Pos.pos' -> XML.tree
-val inputFillFormula: calcID -> string -> XML.tree
+val inputFillFormula: States.calcID -> string -> XML.tree
-val interSteps : calcID -> Pos.pos' -> XML.tree
+val interSteps : States.calcID -> Pos.pos' -> XML.tree
-val Iterator : calcID -> XML.tree
+val Iterator : States.calcID -> XML.tree
-val IteratorTEST : calcID -> iterID
+val IteratorTEST : States.calcID -> States.iterID
-val modelProblem : calcID -> XML.tree
+val modelProblem : States.calcID -> XML.tree
-val modifyCalcHead : calcID -> P_Spec.icalhd -> XML.tree
+val modifyCalcHead : States.calcID -> P_Spec.icalhd -> XML.tree
-val moveActiveCalcHead : calcID -> XML.tree
+val moveActiveCalcHead : States.calcID -> XML.tree
-val moveActiveDown : calcID -> XML.tree
+val moveActiveDown : States.calcID -> XML.tree
-val moveActiveFormula : calcID -> Pos.pos' -> XML.tree
+val moveActiveFormula : States.calcID -> Pos.pos' -> XML.tree
-val moveActiveLevelDown : calcID -> XML.tree
+val moveActiveLevelDown : States.calcID -> XML.tree
-val moveActiveLevelUp : calcID -> XML.tree
+val moveActiveLevelUp : States.calcID -> XML.tree
-val moveActiveRoot : calcID -> XML.tree
+val moveActiveRoot : States.calcID -> XML.tree
-val moveActiveRootTEST : calcID -> XML.tree
+val moveActiveRootTEST : States.calcID -> XML.tree
-val moveActiveUp : calcID -> XML.tree
+val moveActiveUp : States.calcID -> XML.tree
-val moveCalcHead : calcID -> Pos.pos' -> XML.tree
+val moveCalcHead : States.calcID -> Pos.pos' -> XML.tree
-val moveDown : calcID -> Pos.pos' -> XML.tree
+val moveDown : States.calcID -> Pos.pos' -> XML.tree
-val moveLevelDown : calcID -> Pos.pos' -> XML.tree
+val moveLevelDown : States.calcID -> Pos.pos' -> XML.tree
-val moveLevelUp : calcID -> Pos.pos' -> XML.tree
+val moveLevelUp : States.calcID -> Pos.pos' -> XML.tree
-val moveRoot : calcID -> XML.tree
+val moveRoot : States.calcID -> XML.tree
-val moveUp : calcID -> Pos.pos' -> XML.tree
+val moveUp : States.calcID -> Pos.pos' -> XML.tree
-val refFormula : calcID -> Pos.pos' -> XML.tree
+val refFormula : States.calcID -> Pos.pos' -> XML.tree
-val refineProblem : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
+val refineProblem : States.calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
-val replaceFormula : calcID -> TermC.as_string -> XML.tree
+val replaceFormula : States.calcID -> TermC.as_string -> XML.tree
-val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
+val requestFillformula : States.calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
-val resetCalcHead : calcID -> XML.tree
+val resetCalcHead : States.calcID -> XML.tree
-val setMethod : calcID -> MethodC.id -> XML.tree
+val setMethod : States.calcID -> MethodC.id -> XML.tree
-val setNextTactic : calcID -> Tactic.input -> XML.tree
+val setNextTactic : States.calcID -> Tactic.input -> XML.tree
-val setProblem : calcID -> Problem.id -> XML.tree
+val setProblem : States.calcID -> Problem.id -> XML.tree
-val setTheory : calcID -> ThyC.id -> XML.tree
+val setTheory : States.calcID -> ThyC.id -> XML.tree
 end
 (**)
 structure Kernel(**): KERNEL(**) =
 struct
 (*.'Iterator 1' must exist with each CalcTree;
 the only for updating the calc-tree
 WN.0411: only 'Iterator 1' is stored,
 all others are just calculated on the fly
-TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
+TODO: adapt Iterator, States.add_user(= add_iterator!),etc. accordingly .*)
 fun Iterator cI = (*returned ID unnecessary after WN.0411*)
-case \<^try>\<open> (adduserOK2xml cI (add_user cI ))\<close> of
+case \<^try>\<open> (adduserOK2xml cI (States.add_user cI ))\<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 1";
-fun IteratorTEST cI = add_user cI;
+fun IteratorTEST cI = States.add_user cI;
 (* create a calc-tree; compare "fun CalcTreeTEST" *)
 fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
 (case \<^try>\<open>
 	let
 	    val cs = Step_Specify.nxt_specify_init_calc (fmz, sp)
-	    val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
+	    val cI = States.add_calc cs (*FIXME.WN.8.03: error-handling missing*)
 	   in calctreeOK2xml cI end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml 0 "error in kernel 2")
 	| CalcTree [] = raise ERROR "CalcTree: called with []"
 	| CalcTree _ = raise ERROR "CalcTree: undef.case in fun.def"
-fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (del_calc cI);
+fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (States.del_calc cI);
-fun getActiveFormula cI = iteratorOK2xml cI (get_pos cI 1);
+fun getActiveFormula cI = iteratorOK2xml cI (States.get_pos cI 1);
 fun moveActiveFormula cI p =
-let val ((pt,_),_) = get_calc cI
+let val ((pt,_),_) = States.get_calc cI
 in
 if existpt' p pt
-then (upd_ipos cI 1 p; iteratorOK2xml cI p)
+then (States.upd_ipos cI 1 p; iteratorOK2xml cI p)
 else sysERROR2xml cI "frontend sends a non-existing pos"
 end
 (*. set the next tactic to be applied: dont't change the calc-tree,
 but remember the envisaged changes for fun autoCalculate;
 compare force NextTactic .*)
 fun setNextTactic cI tac =
 let
-val ((pt, _), _) = get_calc cI                     (* retrieve Calc.state_pre from states *)
+val ((pt, _), _) = States.get_calc cI                     (* retrieve Calc.state_pre from states *)
-val ip = get_pos cI 1                              (* retrieve position from states  *)
+val ip = States.get_pos cI 1                              (* retrieve position from states  *)
 in
 case Step.by_tactic tac (pt, ip) of
 ("ok", (tacis, _, _)) =>                         (* update Calc.state_pre in states     *)
-(upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
+(States.upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
 	| ("unsafe-ok", (tacis, _, _)) =>
-	    (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
+	    (States.upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
 	| ("not-applicable", _) => setnexttactic2xml cI "not-applicable"
 	| ("end-of-calculation", _) => setnexttactic2xml cI "end-of-calculation"
 	| (msg, _) => sysERROR2xml cI ("setNextTactic: Step.by_tactic returns " ^ msg)
 end;
 (*. apply a tactic at a position and update the calc-tree if applicable .*)
 (*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
 fun applyTactic cI ip tac =
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-	  val p = get_pos cI 1
+	  val p = States.get_pos cI 1
 in
 case Step.by_tactic tac (pt, ip) of
 	    ("ok", (_, c, ptp as (_, p'))) =>
-	      (upd_calc cI (ptp, []);
+	      (States.upd_calc cI (ptp, []);
-	       upd_ipos cI 1 p';
+	       States.upd_ipos cI 1 p';
 	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
 	  | ("unsafe-ok", (_, c, ptp as (_, p'))) =>
-	      (upd_calc cI (ptp, []);
+	      (States.upd_calc cI (ptp, []);
-	       upd_ipos cI 1 p';
+	       States.upd_ipos cI 1 p';
 	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
 	  | ("end-of-calculation", (_, c, ptp as (_, p'))) =>
-	      (upd_calc cI (ptp, []);
+	      (States.upd_calc cI (ptp, []);
-	       upd_ipos cI 1 p';
+	       States.upd_ipos cI 1 p';
 	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
 	  | (str, _) => autocalculateERROR2xml cI ("applyTactic: Step.by_tactic returns " ^ str)
 end;
 fun fetchProposedTactic cI =
 case \<^try>\<open>
-(case Step.do_next (get_pos cI 1) (get_calc cI) of
+(case Step.do_next (States.get_pos cI 1) (States.get_calc cI) of
 	  ("ok", (tacis, _, _)) =>
 	  let
-	    val _ = upd_tacis cI tacis
+	    val _ = States.upd_tacis cI tacis
 	    val (tac, _, _) = last_elem tacis
 	  in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
 	| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
 	| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
 	| ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation"
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 3";
 fun autoCalculate cI auto = (*Future.fork
 (fn () => (( *)let
-val pold = get_pos cI 1
+val pold = States.get_pos cI 1
 in
-case Math_Engine.autocalc [] pold (get_calc cI) auto of
+case Math_Engine.autocalc [] pold (States.get_calc cI) auto of
 ("ok", c, ptp as (_,p)) =>
-(upd_calc cI (ptp, []); upd_ipos cI 1 p;
+(States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
 | ("dummy", c, ptp as (_,p)) => (*prelim. until \<open>Review modelling- + specification-phase\<close>*)
-(upd_calc cI (ptp, []); upd_ipos cI 1 p;
+(States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
 | ("end-of-calculation", c, ptp as (_,p)) =>
-(upd_calc cI (ptp, []); upd_ipos cI 1 p;
+(States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
 | (str, _, _) => autocalculateERROR2xml cI str
 end (* ) *)
 handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);
 fun getTactic cI (p:pos') =
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 val (_, tac, _) = ME_Misc.pt_extract (pt, p)
 in
 case tac of
 	    SOME ta => gettacticOK2xml cI ta
 	  | NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)
 @see #TACTICS_CURRENT_METHOD  ..the only impl.WN040307
 LItool.specific_from_prog waits to be used here
 *)
 fun fetchApplicableTactics cI (_(*scope*): int) (p : pos') =
 case \<^try>\<open>
-let val ((pt, _), _) = get_calc cI
+let val ((pt, _), _) = States.get_calc cI
 in (applicabletacticsOK cI (Fetch_Tacs.from_prog pt p))
 handle PTREE str => sysERROR2xml cI str
 end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 5";
 fun getAssumptions cI (p:pos') =
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 	  val (_, _, asms) = ME_Misc.pt_extract (pt, p)
 in getasmsOK2xml cI asms end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "syserror in getAssumptions"
 (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
 fun getAccumulatedAsms cI (p:pos') =
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 val ass = Ctree.get_assumptions pt p
 in getasmsOK2xml cI ass end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "syserror in getAccumulatedAsms"
 fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 	  val (form, _, _) = ME_Misc.pt_extract (pt, p)
 in refformulaOK2xml cI p form end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)
 "from" "to" are designed for use by iterators of calcChangedEvent,
 thus "from" is the last unchanged position *)
 fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =
 (case \<^try>\<open>
 let
-val ((pt,_),_) = get_calc cI
+val ((pt,_),_) = States.get_calc cI
 val headline =
 case ME_Misc.pt_extract (pt, to) of
 (ModSpec (_, _, headline, _, _, _), _, _) => headline
 | _ => raise ERROR "getFormulaeFromTo: uncovered case of ME_Misc.pt_extract"
 in getintervalOK cI [(to, headline, NONE)] end
 (case from of
 ([], Res) => sysERROR2xml cI ("getFormulaeFromTo does: moveDown " ^
 "from=([],Res) .. goes beyond result")
 | _ =>
 let
-val ((pt,_),_) = get_calc cI
+val ((pt,_),_) = States.get_calc cI
 val f = move_dn [] pt from
 fun max (a,b) = if a < b then b else a
 val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
 in getintervalOK cI (ME_Misc.get_interval f to lev pt) end)
 \<close> of
 sysERROR2xml cI ("getFormulaeFromTo impl.for formulae only, " ^
 "i.e. last arg only impl. for false, _NOT_ true");
 fun interSteps cI ip =
 case \<^try>\<open>
-let val ((pt, p), tacis) = get_calc cI
+let val ((pt, p), tacis) = States.get_calc cI
 in
 if (not o is_interpos) ip
 then interStepsERROR cI ("only formulae with position (_,Res) " ^
 "may have intermediate steps above them")
 else
 let val ip' = lev_pred' pt ip
 in case Detail_Step.go pt ip of
 ("detailrls", pt, lastpos) =>
-(upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
+(States.upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
 | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
 | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
 end
 end
 \<close> of
 | NONE => sysERROR2xml cI "error in kernel 8";
 fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Spec.icalhd) =
 case \<^try>\<open>
 let
-val ((pt,_),_) = get_calc cI
+val ((pt,_),_) = States.get_calc cI
 val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd
-in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end
+in (States.upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 9";
 (* at the activeFormula set the Model, the Guard and the Specification to empty
 and return a CalcHead; the 'origin' remains (for reconstructing all that) *)
 fun resetCalcHead cI =
 case \<^try>\<open>
 let
-val (ptp,_) = get_calc cI
+val (ptp,_) = States.get_calc cI
 val ptp = SpecificationC.reset ptp
-in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
+in (States.upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 10";
 (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
 the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
 fun modelProblem cI =
 case \<^try>\<open>
-let val (ptp, _) = get_calc cI
+let val (ptp, _) = States.get_calc cI
 	val ptp = SpecificationC.reset ptp
 	val (_, (_, _, ptp)) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
-in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
+in (States.upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 11";
 (* specify the MethodC at the activeFormula and return a CalcHead containing the Guard.
 WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
 fun setMethod cI mI =
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-val ip as (_, p_) = get_pos cI 1
+val ip as (_, p_) = States.get_pos cI 1
 in
 if member op = [Pbl,Met] p_
 then
 let val (pt, chd) = Math_Engine.set_method mI (pt, ip)
-in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
+in (States.upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
 else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
 end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 12";
 (* specify the Problem at the activeFormula and return a CalcHead containing the Model;
 special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Problem" *)
 fun setProblem cI pI =
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-val ip as (_, p_) = get_pos cI 1
+val ip as (_, p_) = States.get_pos cI 1
 in
 if member op = [Pbl,Met] p_
 then
 let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
-	    in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
+	    in (States.upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
 end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 13";
 (* specify the Theory at the activeFormula and return a CalcHead;
 special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
 fun setTheory cI tI =
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-val ip as (_, p_) = get_pos cI 1
+val ip as (_, p_) = States.get_pos cI 1
 in
 if member op = [Pbl,Met] p_
 then
 let val (pt, chd) = Math_Engine.set_theory tI (pt, ip)
-in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
+in (States.upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
 end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 14";
 Not used in isac-java (see comment WN0825 for setContext) but tryrefine is used within isabisac *)
 fun refineProblem cI (p, p_) guh =
 case \<^try>\<open>
 let
 val pblID = Ptool.guh2kestoreID guh
-	  val ((pt,_),_) = get_calc cI
+	  val ((pt,_),_) = States.get_calc cI
 	  val pp = par_pblobj pt p
 	  val chd = Math_Engine.tryrefine pblID pt (pp, p_)
 in contextpblOK2xml cI chd end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 16";
 (* append a formula to the calculation *)
 fun appendFormula' cI (ifo: TermC.as_string) =
 (let
-val cs = get_calc cI
+val cs = States.get_calc cI
-val pos = get_pos cI 1
+val pos = States.get_pos cI 1
 in
 case Step.do_next pos cs of
 	    ("ok", (_, _, ptp)) =>
 	      (case Step_Solve.by_term ptp (encode ifo) of
 	        ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
-	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;
+	          (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
 	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
 	      | ("same-formula", (_, c, ptp as (_, p))) =>
-	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;
+	          (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
 	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
 	      | (msg, _) => appendformulaERROR2xml cI msg)
 	  | (msg, _) => appendformulaERROR2xml cI msg
 end)
 handle ERROR msg => sysERROR2xml cI ("error in kernel 17: " ^ msg);
 (* replace a formula with_in_ a calculation; this applies for initial CAS-commands, too *)
 fun replaceFormula cI ifo =
 case \<^try>\<open>
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-val p = get_pos cI 1
+val p = States.get_pos cI 1
 in
 case Step_Solve.by_term (pt, p) (encode ifo) of
 	    ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
 	      let
 	        val unc = if null (fst p) then p else move_up [] pt p
-	        val _ = upd_calc cI (ptp', [])
+	        val _ = States.upd_calc cI (ptp', [])
-	        val _ = upd_ipos cI 1 p'
+	        val _ = States.upd_ipos cI 1 p'
 	      in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end
 	  | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"
 	  | (msg, _) => replaceformulaERROR2xml cI msg
 end
 \<close> of
 move*:       compute the new iterator from the old one on the fly
 ***)
 fun moveActiveRoot cI =
 case \<^try>\<open>
-let val _ = upd_ipos cI 1 ([], Pbl)
+let val _ = States.upd_ipos cI 1 ([], Pbl)
 in iteratorOK2xml cI ([], Pbl) end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 19"
 fun moveRoot cI =
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "";
 fun moveActiveRootTEST cI =
 case \<^try>\<open>
-let val _ = upd_ipos cI 1 ([], Pbl)
+let val _ = States.upd_ipos cI 1 ([], Pbl)
 in iteratorOK2xml cI ([], Pbl) end
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 20"
 fun moveActiveDown cI =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-	  val ip' = move_dn [] pt (get_pos cI 1)
+	  val ip' = move_dn [] pt (States.get_pos cI 1)
-	  val _ = upd_ipos cI 1 ip'
+	  val _ = States.upd_ipos cI 1 ip'
 in iteratorOK2xml cI ip' end)
 handle (PTREE _) => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 21"
 fun moveDown cI p =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 	  val ip' = move_dn [] pt p
 in iteratorOK2xml cI ip' end)
 handle (PTREE _) => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 22"
 fun moveActiveLevelDown cI =
 case \<^try>\<open>
 (let
-val ((pt, _) ,_) = get_calc cI
+val ((pt, _) ,_) = States.get_calc cI
-	val ip' = movelevel_dn [] pt (get_pos cI 1)
+	val ip' = movelevel_dn [] pt (States.get_pos cI 1)
-	val _ = upd_ipos cI 1 ip'
+	val _ = States.upd_ipos cI 1 ip'
 in iteratorOK2xml cI ip' end)
 handle (PTREE _) => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 23"
 fun moveLevelDown cI p =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 val ip' = movelevel_dn [] pt p
 in iteratorOK2xml cI ip' end)
 handle (PTREE _) => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 24"
 fun moveActiveUp cI =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-	  val ip' = move_up [] pt (get_pos cI 1)
+	  val ip' = move_up [] pt (States.get_pos cI 1)
-	  val _ = upd_ipos cI 1 ip'
+	  val _ = States.upd_ipos cI 1 ip'
 in iteratorOK2xml cI ip' end)
 handle PTREE _ => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 25"
 fun moveUp cI p =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 	  val ip' = move_up [] pt p
 in iteratorOK2xml cI ip' end)
 handle PTREE _ => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 26"
 fun moveActiveLevelUp cI =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-val ip' = movelevel_up [] pt (get_pos cI 1)
+val ip' = movelevel_up [] pt (States.get_pos cI 1)
-val _ = upd_ipos cI 1 ip'
+val _ = States.upd_ipos cI 1 ip'
 in iteratorOK2xml cI ip' end)
 handle PTREE _ => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 27"
 fun moveLevelUp cI p =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 	  val ip' = movelevel_up [] pt p
 in iteratorOK2xml cI ip' end)
 handle PTREE _ => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 28"
 fun moveActiveCalcHead cI =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-	  val ip' = movecalchd_up pt (get_pos cI 1)
+	  val ip' = movecalchd_up pt (States.get_pos cI 1)
-	  val _ = upd_ipos cI 1 ip'
+	  val _ = States.upd_ipos cI 1 ip'
 in iteratorOK2xml cI ip' end)
 handle PTREE _ => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 | NONE => sysERROR2xml cI "error in kernel 29"
 fun moveCalcHead cI p =
 case \<^try>\<open>
 (let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
 	  val ip' = movecalchd_up pt p
 in iteratorOK2xml cI ip' end)
 handle PTREE _ => iteratorERROR2xml cI
 \<close> of
 SOME xml => xml
 for an Error_Pattern.id find "(fill_in_id * fill_in) list"
 which is applicable to the current formula.
 *)
 fun findFillpatterns cI errpatID =
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-		val pos = get_pos cI 1;
+		val pos = States.get_pos cI 1;
 		val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID
 in findFillpatterns2xml cI (map #1 fillpats) end
 (* given a fillpatID propose a fillform to the learner on the worksheet;
 the "ctree" is extended with fillpat and "ostate Inconsistent",
 returns CalcChanged.
 arg errpatID: required because there is no dialog-related state in the math-kernel.
 *)
 fun requestFillformula cI (errpatID, fillpatID) =
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-		val pos = get_pos cI 1
+		val pos = States.get_pos cI 1
 val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID
 in
 case filter ((curry op = fillpatID) o
 (#1: (Error_Pattern_Def.fill_in_id * term * thm * (Subst.input option) -> Error_Pattern_Def.fill_in_id))) fillforms of
 (_, fillform, thm, sube_opt) :: _ =>
 let
 val (pt, pos') = Step.inconsistent (sube_opt, ThmC.of_thm thm)
 fillform (get_loc pt pos) pos pt
 in
-(upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
+(States.upd_calc cI ((pt, pos'), []); (*States.upd_ipos cI 1 pos';*)
 autocalculateOK2xml cI pos pos' pos')
 end
 | _ => autocalculateERROR2xml cI "no fillpattern found"
 end;
 presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
 errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
 The respective thm is stored in the ctree. *)
 fun inputFillFormula cI ifo =
 let
-val ((pt, _), _) = get_calc cI
+val ((pt, _), _) = States.get_calc cI
-val pos = get_pos cI 1;
+val pos = States.get_pos cI 1;
 in
 case Error_Pattern.filled_exactly (pt, pos) ifo of
 ("ok", tac) =>
 let
 in (* cp from applyTactic *)
 case Step.by_tactic tac (pt, pos) of
 ("ok", (_, c, ptp as (_,p'))) =>
-(upd_calc cI (ptp, []);
+(States.upd_calc cI (ptp, []);
-upd_ipos cI 1 p';
+States.upd_ipos cI 1 p';
 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
 | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
-(upd_calc cI (ptp, []);
+(States.upd_calc cI (ptp, []);
-upd_ipos cI 1 p';
+States.upd_ipos cI 1 p';
 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
 | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
-(upd_calc cI (ptp, []);
+(States.upd_calc cI (ptp, []);
-upd_ipos cI 1 p';
+States.upd_ipos cI 1 p';
 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
 | _ => autocalculateERROR2xml cI "failure"
 end
 | (msg, _) => message2xml cI msg
 end

changeset 60549	c0a775618258
parent 60266	4921574fd67f
child 60557	0be383bdb883