1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Sun Jan 08 12:33:27 2023 +0100
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Sun Jan 08 16:19:31 2023 +0100
     1.3 @@ -265,7 +265,7 @@
     1.4      XML.Elem (("ASM", []), [xml_of_term asm]),
     1.5      XML.Elem (("VALUE", []), [xml_of_term vl])])
     1.6  
     1.7 -fun xml_of_matchpbl (model_ok, pI, hdl, pbl, where_) =
     1.8 +fun xml_of_matchpbl (model_ok, _(*pI*), hdl, pbl, where_) =
     1.9    XML.Elem (("CONTEXTDATA", []), [
    1.10      XML.Elem (("GUH", []), [(XML.Text "would-need-ctxt")(*XML.Text (Ptool.pblID2guh pI)*)]),
    1.11      XML.Elem (("STATUS", []), [

     2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml	Sun Jan 08 12:33:27 2023 +0100
     2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml	Sun Jan 08 16:19:31 2023 +0100
     2.3 @@ -141,24 +141,28 @@
     2.4    end;
     2.5  
     2.6  fun fetchProposedTactic cI =
     2.7 -  case \<^try>\<open>
     2.8 -    (case Step.do_next (States.get_pos cI 1) (States.get_calc cI) of
     2.9 -  	  ("ok", (tacis, _, _)) =>
    2.10 -    	  let
    2.11 -    	    val _ = States.upd_tacis cI tacis
    2.12 -    	    val (tac, _, _) = last_elem tacis
    2.13 -    	  in 
    2.14 -    	    fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store 
    2.15 -    	      (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge")) tac)
    2.16 -    	        (*ctxt shall become an argument ^^^^^^^^ of fetchProposedTactic*)
    2.17 -        end
    2.18 -  	| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
    2.19 -  	| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
    2.20 -  	| ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation"
    2.21 -    | _ => raise ERROR "fetchProposedTactic: undef.case")
    2.22 -    \<close> of
    2.23 -    SOME xml => xml
    2.24 -  | NONE => sysERROR2xml cI "error in kernel 3";
    2.25 +  let
    2.26 +    val pos = States.get_pos cI 1
    2.27 +    val state_pre as ((pt, _), _) = States.get_calc cI
    2.28 +    val ctxt = Ctree.get_ctxt pt pos
    2.29 +  in
    2.30 +    case \<^try>\<open>
    2.31 +      (case Step.do_next pos state_pre of
    2.32 +    	  ("ok", (tacis, _, _)) =>
    2.33 +      	  let
    2.34 +      	    val _ = States.upd_tacis cI tacis
    2.35 +      	    val (tac, _, _) = last_elem tacis
    2.36 +      	  in 
    2.37 +      	    fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store ctxt tac)
    2.38 +          end
    2.39 +    	| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
    2.40 +    	| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
    2.41 +    	| ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation"
    2.42 +      | _ => raise ERROR "fetchProposedTactic: undef.case")
    2.43 +      \<close> of
    2.44 +      SOME xml => xml
    2.45 +  | NONE => sysERROR2xml cI "error in kernel 3"
    2.46 +  end;
    2.47  
    2.48  fun autoCalculate cI auto = (*Future.fork
    2.49    (fn () => (( *)let
    2.50 @@ -178,7 +182,7 @@
    2.51    end (* ) *)
    2.52    handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);
    2.53  
    2.54 -fun getTactic cI (p:pos') =
    2.55 +fun getTactic cI (_: pos') =
    2.56    case \<^try>\<open>
    2.57      let 
    2.58        val ((pt, p), _) = States.get_calc cI
    2.59 @@ -210,7 +214,7 @@
    2.60      SOME xml => xml
    2.61    | NONE => sysERROR2xml cI "error in kernel 5";
    2.62  
    2.63 -fun getAssumptions cI (p:pos') =
    2.64 +fun getAssumptions cI (_: pos') =
    2.65    case \<^try>\<open>
    2.66      let 
    2.67        val ((pt, p), _) = States.get_calc cI

     3.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Sun Jan 08 12:33:27 2023 +0100
     3.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Sun Jan 08 16:19:31 2023 +0100
     3.3 @@ -154,7 +154,8 @@
     3.4    which is stored at the pos where the input is stored of "ok".
     3.5  *)
     3.6  fun filled_exactly (pt, pos as (p, _)) istr =
     3.7 -  case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr of
     3.8 +  (* input from Isabelle/PIDE: TODO handle Position *)
     3.9 +  case TermC.parseNEW (Ctree.get_ctxt pt pos) istr of
    3.10      NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
    3.11    | SOME ifo => 
    3.12        let

     4.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Sun Jan 08 12:33:27 2023 +0100
     4.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Sun Jan 08 16:19:31 2023 +0100
     4.3 @@ -122,8 +122,11 @@
     4.4          | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj"
     4.5          val {where_, ...} = Problem.from_store ctxt pI
     4.6          val pres = map (I_Model.environment probl |> subst_atomic) where_
     4.7 -        val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
     4.8 -          then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
     4.9 +        val ctxt = if ContextC.is_empty ctxt (*only in case of input by user*)
    4.10 +          then dI 
    4.11 +            |> Know_Store.get_via_last_thy
    4.12 +            |> Proof_Context.init_global
    4.13 +            |> ContextC.insert_assumptions pres
    4.14            else ctxt
    4.15        in
    4.16          Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))

     5.1 --- a/src/Tools/isac/MathEngBasic/calculation.sml	Sun Jan 08 12:33:27 2023 +0100
     5.2 +++ b/src/Tools/isac/MathEngBasic/calculation.sml	Sun Jan 08 16:19:31 2023 +0100
     5.3 @@ -15,6 +15,7 @@
     5.4  
     5.5    type state_pre
     5.6    type state_post
     5.7 +
     5.8  \<^isac_test>\<open>
     5.9  (*val state_pre_empty: state_pre*)
    5.10    val state_empty_pre: state_pre