1.1 --- a/src/Tools/isac/Test_Code/test-code.sml	Fri Oct 21 15:35:50 2022 +0200
     1.2 +++ b/src/Tools/isac/Test_Code/test-code.sml	Sun Oct 23 16:08:27 2022 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    type NEW (* TODO: refactor "fun me" with Calc.state_pre and remove *)
     1.6    val f2str : Test_Out.mout -> TermC.as_string
     1.7 -  val TESTg_form : Calc.T -> Test_Out.mout
     1.8 +  val TESTg_form : Proof.context -> Calc.T -> Test_Out.mout
     1.9  
    1.10    val init_calc : Proof.context -> Formalise.T list -> Pos.pos' * NEW * Test_Out.mout * Tactic.input * Celem.safe * Ctree.ctree
    1.11    val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
    1.12 @@ -37,9 +37,9 @@
    1.13  
    1.14  (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
    1.15     delete as soon as TESTg_form -> _mout_ dropped           *)
    1.16 -fun TESTg_form ptp =
    1.17 +fun TESTg_form ctxt ptp =
    1.18    let
    1.19 -    val (form, _, _) = ME_Misc.pt_extract ptp
    1.20 +    val (form, _, _) = ME_Misc.pt_extract ctxt ptp
    1.21    in
    1.22      case form of
    1.23        Ctree.Form t => Test_Out.FormKF (UnparseC.term t)
    1.24 @@ -48,7 +48,7 @@
    1.25          (case p_ of Pos.Pbl => Test_Out.Problem []
    1.26            | Pos.Met => Test_Out.MethodC []
    1.27            | _ => raise ERROR "TESTg_form: uncovered case",
    1.28 - 			P_Model.from (ThyC.get_theory"Isac_Knowledge") gfr pre))
    1.29 + 			P_Model.from (Proof_Context.theory_of ctxt) gfr pre))
    1.30     end
    1.31  (* for quick test-print-out, until 'type inout' is removed *)
    1.32  fun f2str (Test_Out.FormKF cterm') = cterm'
    1.33 @@ -60,13 +60,14 @@
    1.34      val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
    1.35      val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
    1.36  	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
    1.37 -	  val f = TESTg_form (pt,p)
    1.38 +	  val f = TESTg_form ctxt (pt,p)
    1.39    in (p, []:NEW, f, tac, Celem.Sundef, pt) end
    1.40  | init_calc _ _ = raise ERROR "Tess_Code.init_calc: uncovered case"
    1.41         
    1.42  fun me (*(Empty_Tac) p _ _ = raise ERROR ("me:  Empty_Tac at " ^ pos'2str p)
    1.43    | me*) tac p _(*NEW remove*) pt =
    1.44 -    let 
    1.45 +    let
    1.46 +      val ctxt = Ctree.get_ctxt pt p
    1.47        val (pt, p) = 
    1.48    	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
    1.49    	    case Step.by_tactic tac (pt, p) of
    1.50 @@ -90,7 +91,7 @@
    1.51            tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 
    1.52    		  | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
    1.53      in
    1.54 -      (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *), 
    1.55 +      (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *), 
    1.56    	    tac, Celem.Sundef, pt)
    1.57      end
    1.58  
    1.59 @@ -134,6 +135,7 @@
    1.60  fun me_trace (*(Empty_Tac) p _ _ = raise ERROR ("me:  Empty_Tac at " ^ pos'2str p)
    1.61    | me*) (pt, p) tac trace =
    1.62      let
    1.63 +      val ctxt = Ctree.get_ctxt pt p
    1.64        val _ = if quiet tac then () else
    1.65          writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");
    1.66        val (pt', p') = 
    1.67 @@ -161,7 +163,7 @@
    1.68          writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.input_to_string tac'' ^ "----------------------------------");
    1.69        val _ = trace (pt'', p'') tac
    1.70      in
    1.71 -      ((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))
    1.72 +      ((pt', p'), tac'', TESTg_form ctxt (pt', p') (* form output comes from Step.by_tactic *))
    1.73      end
    1.74  
    1.75  fun tac2tac_ pt p m =