1.1 --- a/src/Tools/isac/Interpret/istate.sml	Mon Jan 09 16:40:54 2023 +0100
     1.2 +++ b/src/Tools/isac/Interpret/istate.sml	Tue Jan 10 10:01:05 2023 +0100
     1.3 @@ -13,9 +13,9 @@
     1.4  
     1.5    datatype T = datatype Istate_Def.T
     1.6    val empty: T
     1.7 -  val string_of: T -> string
     1.8 +  val string_of: Proof.context -> T -> string
     1.9    val string_of': T -> string
    1.10 -  val istates2str: T option * T option -> string
    1.11 +  val istates2str: Proof.context -> T option * T option -> string
    1.12    val the_pstate: T -> pstate
    1.13  
    1.14    val init_detail: Proof.context -> Tactic.input -> term -> Istate_Def.T

     2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Mon Jan 09 16:40:54 2023 +0100
     2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Tue Jan 10 10:01:05 2023 +0100
     2.3 @@ -281,8 +281,8 @@
     2.4              end
     2.5          | _ => End_Program (Pstate ist, Tactic.End_Detail' (TermC.empty,[])))
     2.6      | Reject_Tac => Helpless)
     2.7 -  | find_next_step _ _ ist _ =
     2.8 -    raise ERROR ("find_next_step: not impl for " ^ Istate.string_of ist);
     2.9 +  | find_next_step _ _ ist ctxt =
    2.10 +    raise ERROR ("find_next_step: not impl for " ^ Istate.string_of ctxt ist);
    2.11  
    2.12  
    2.13  (*** locate an input tactic within a program ***)

     3.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml	Mon Jan 09 16:40:54 2023 +0100
     3.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml	Tue Jan 10 10:01:05 2023 +0100
     3.3 @@ -16,9 +16,9 @@
     3.4  
     3.5    datatype T = RrlsState of Rule_Set.rrlsstate | Pstate of pstate | Uistate
     3.6    val empty: T
     3.7 -  val string_of: T -> string
     3.8 +  val string_of: Proof.context -> T -> string
     3.9    val string_of': T -> string
    3.10 -  val istates2str: T option * T option -> string
    3.11 +  val istates2str: Proof.context -> T option * T option -> string
    3.12  
    3.13    val set_eval: Rule_Set.T -> pstate -> pstate
    3.14    val set_act: term -> pstate -> pstate
    3.15 @@ -85,22 +85,25 @@
    3.16    | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*)
    3.17  val empty = Pstate e_pstate;
    3.18  
    3.19 -fun rta2str (r, (t, a)) = "\n(" ^ Rule.to_string r ^ ", (" ^ UnparseC.term t ^ ", " ^ UnparseC.terms a ^ "))";
    3.20 -fun string_of Uistate = "Uistate"
    3.21 -  | string_of (Pstate pst) = 
    3.22 -    "Pstate " ^ pstate2str pst
    3.23 -  | string_of (RrlsState (t, t1, rss, rtas)) =
    3.24 -    "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term t1 ^ ", " ^
    3.25 -    (strs2str o (map (strs2str o (map Rule.to_string)))) rss ^ ", " ^
    3.26 -    (strs2str o (map rta2str)) rtas ^ ")";
    3.27 +fun rta2str ctxt (r, (t, a)) =
    3.28 +  "\n(" ^ Rule.to_string_PIDE ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^
    3.29 +  UnparseC.terms_in_ctxt ctxt a ^ "))";
    3.30 +fun string_of _ Uistate = "Uistate"
    3.31 +  | string_of _ (Pstate pst) = 
    3.32 +    "Pstate " ^ pstate2str pst   
    3.33 +  | string_of ctxt (RrlsState (t, t1, rss, rtas)) =
    3.34 +    "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^
    3.35 +    (strs2str o (map (strs2str o (map (Rule.to_string_PIDE ctxt))))) rss ^ ", " ^
    3.36 +    (strs2str o (map (rta2str ctxt))) rtas ^ ")";
    3.37  fun string_of' Uistate = "Uistate"
    3.38    | string_of' (Pstate pst) = 
    3.39      "Pstate " ^ pstate2str' pst
    3.40    | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState"
    3.41 -fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
    3.42 -  | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ist ^ ")"
    3.43 -  | istates2str (SOME ist, NONE) = "(#SOME " ^ string_of ist ^ ",\n #NONE)"
    3.44 -  | istates2str (SOME i1, SOME i2) = "(#SOME " ^ string_of i1 ^ ",\n #SOME " ^ string_of i2 ^ ")";
    3.45 +fun istates2str _ (NONE, NONE) = "(#NONE, #NONE)"
    3.46 +  | istates2str ctxt (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ctxt ist ^ ")"
    3.47 +  | istates2str ctxt (SOME ist, NONE) = "(#SOME " ^ string_of ctxt ist ^ ",\n #NONE)"
    3.48 +  | istates2str ctxt (SOME i1, SOME i2) =
    3.49 +    "(#SOME " ^ string_of ctxt i1 ^ ",\n #SOME " ^ string_of ctxt i2 ^ ")";
    3.50  
    3.51  
    3.52  fun set_eval e {env, path, form_arg, act_arg, or, found_accept, assoc, ...} =

     4.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Mon Jan 09 16:40:54 2023 +0100
     4.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Tue Jan 10 10:01:05 2023 +0100
     4.3 @@ -39,7 +39,7 @@
     4.4  val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
     4.5  fun taci2str ctxt ((tac, tac_, (pos', (istate, _))): single) =
     4.6    "( " ^ Tactic.input_to_string ctxt tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
     4.7 -  Istate_Def.string_of istate ^ " ))"
     4.8 +  Istate_Def.string_of ctxt istate ^ " ))"
     4.9  
    4.10  type T = single list;
    4.11  

     5.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Mon Jan 09 16:40:54 2023 +0100
     5.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Tue Jan 10 10:01:05 2023 +0100
     5.3 @@ -156,7 +156,7 @@
     5.4  
     5.5   val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1; (*<---------------------- orig. test code*)
     5.6  (*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"
     5.7 -andalso Istate.string_of (get_istate_LI pt p)
     5.8 +andalso Istate.string_of ctxt (get_istate_LI pt p)
     5.9    = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
    5.10  then () else error "refFormula =   1 + - 1 * 2 + x = 0   changed";
    5.11  (*-------------------------------------------------------------------------*)
    5.12 @@ -176,11 +176,11 @@
    5.13  
    5.14  (*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
    5.15  Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
    5.16 -if Istate.string_of istate
    5.17 +if Istate.string_of ctxt istate
    5.18   = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
    5.19  then () else error "from Step.by_tactic return --- changed 1";
    5.20  
    5.21 -if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
    5.22 +if Istate.string_of ctxt (get_istate_LI (fst cstate) (snd cstate))
    5.23   = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
    5.24  then () else error "from Step.by_tactic return --- changed 2";
    5.25  (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
    5.26 @@ -199,7 +199,7 @@
    5.27  
    5.28  (*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
    5.29  (********************* locate_input_tactic returns cstate * istate * Proof.context  *************)
    5.30 -(*+*)if Istate.string_of istate
    5.31 +(*+*)if Istate.string_of ctxt istate
    5.32  (*+isa*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
    5.33  then case m of Rewrite_Set_Inst' _ => ()
    5.34  else error "from locate_input_tactic return --- changed";
    5.35 @@ -225,7 +225,7 @@
    5.36  
    5.37  (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
    5.38       Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
    5.39 -(*+*)if pos' = ([1], Res) andalso Istate.string_of istate
    5.40 +(*+*)if pos' = ([1], Res) andalso Istate.string_of ctxt istate
    5.41   = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
    5.42  then () else error "init. step 1 + - 1 * 2 + x = 0 changed";
    5.43  
    5.44 @@ -237,7 +237,7 @@
    5.45  (*//------------------------------------- final test -----------------------------------------\\*)
    5.46  val ("ok", [], ptp as (pt, p)) = xxxx;
    5.47                                           
    5.48 -if Istate.string_of (get_istate_LI pt p) (*                <>                 <>                 <>                 <>                     \<up> \<up> \<up> \<up> ^*)
    5.49 +if Istate.string_of ctxt (get_istate_LI pt p) (*                <>                 <>                 <>                 <>                     \<up> \<up> \<up> \<up> ^*)
    5.50  (*REP*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
    5.51  then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"
    5.52  

     6.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Mon Jan 09 16:40:54 2023 +0100
     6.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Tue Jan 10 10:01:05 2023 +0100
     6.3 @@ -662,7 +662,7 @@
     6.4  spec;
     6.5  writeln (I_Model.to_string ctxt probl);
     6.6  writeln (I_Model.to_string ctxt meth);
     6.7 -writeln (Istate.string_of (fst istate));
     6.8 +writeln (Istate.string_of ctxt (fst istate));
     6.9  
    6.10  refFormula 1 ([],Pbl) (*--> correct CalcHead*);
    6.11   (*081016 NOT necessary (but leave it in Java):*)
    6.12 @@ -674,7 +674,7 @@
    6.13  (*val p = ([], Pbl)*)
    6.14  val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
    6.15  val (SOME istate, NONE) = loc;
    6.16 -(*default_print_depth 5;*) writeln (Istate.string_of (fst istate));  (*default_print_depth 3;*)
    6.17 +(*default_print_depth 5;*) writeln (Istate.string_of ctxt (fst istate));  (*default_print_depth 3;*)
    6.18  (*Pstate ([],
    6.19   [], NONE,
    6.20   ??.empty, Sundef, false)*)
    6.21 @@ -719,7 +719,7 @@
    6.22  val ((pt,_),_) = States.get_calc 1;
    6.23  val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
    6.24  val (SOME istate, NONE) = loc;
    6.25 -(*default_print_depth 5;*) writeln (Istate.string_of (fst istate));  (*default_print_depth 3;*)
    6.26 +(*default_print_depth 5;*) writeln (Istate.string_of ctxt (fst istate));  (*default_print_depth 3;*)
    6.27  (*Pstate ([],
    6.28   [], NONE,
    6.29   ??.empty, Sundef, false)*)

     7.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml	Mon Jan 09 16:40:54 2023 +0100
     7.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml	Tue Jan 10 10:01:05 2023 +0100
     7.3 @@ -67,7 +67,7 @@
     7.4       "\n  (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4))",
     7.5       "substitution (y 0 = 0)", "equality equ'''"] then ()
     7.6  else error "biegelinie.sml met setzeRandbed*Ein bb";
     7.7 -(writeln o Istate.string_of) (get_istate_LI pt p);
     7.8 +(writeln o Istate.string_of ctxt) (get_istate_LI pt p);
     7.9  "--- after 1.subpbl [Equation, fromFunction]";
    7.10  
    7.11  val (p,_,f,nxt,_,pt) = me nxt p c pt;

     8.1 --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml	Mon Jan 09 16:40:54 2023 +0100
     8.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml	Tue Jan 10 10:01:05 2023 +0100
     8.3 @@ -50,7 +50,7 @@
     8.4  (*+*)if f2str f =
     8.5    "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^
     8.6    " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error "";
     8.7 -(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) =
     8.8 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt) =
     8.9     "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)";
    8.10  
    8.11  val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
    8.12 @@ -60,7 +60,7 @@
    8.13  
    8.14  (*+isa==isa2*)val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;
    8.15    val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2], ORundef, true, false)" =
    8.16 -(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
    8.17 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
    8.18  
    8.19  case nxt of
    8.20      (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
    8.21 @@ -77,7 +77,7 @@
    8.22  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    8.23  
    8.24    val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
    8.25 -(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
    8.26 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
    8.27  
    8.28  val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f;
    8.29  (*/------------------- step into me Apply_Method -------------------------------------------\*)
    8.30 @@ -92,16 +92,16 @@
    8.31  (*+isa==isa2*)val ([5], Met) = p;
    8.32  (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);
    8.33    val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
    8.34 -(*+isa==isa2*)is1 |> Istate.string_of;
    8.35 +(*+isa==isa2*)is1 |> Istate.string_of ctxt;
    8.36    val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
    8.37 -(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
    8.38 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
    8.39  
    8.40    (*case*)
    8.41        Step.check tac (pt, p) (*of*);
    8.42  "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );
    8.43  
    8.44  (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
    8.45 -(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);
    8.46 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);
    8.47  
    8.48    (*if*) Tactic.for_specify tac (*else*);
    8.49  val Applicable.Yes xxx =
    8.50 @@ -109,7 +109,7 @@
    8.51  Solve_Step.check tac (ctree, pos);
    8.52  
    8.53  (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
    8.54 -(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);
    8.55 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);
    8.56  
    8.57  "~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);
    8.58  	    (*if*)  Tactic.for_specify' tac' (*else*);
    8.59 @@ -119,7 +119,7 @@
    8.60    = (tac', ptp);
    8.61  
    8.62  (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
    8.63 -(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
    8.64 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
    8.65  
    8.66          LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
    8.67  "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
    8.68 @@ -133,7 +133,7 @@
    8.69             (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
    8.70  
    8.71  (*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" =
    8.72 -(*+isa==isa2*)is |> Istate.string_of
    8.73 +(*+isa==isa2*)is |> Istate.string_of ctxt
    8.74  
    8.75          val ini = LItool.implicit_take prog env;
    8.76          val pos = start_new_level pos
    8.77 @@ -144,7 +144,7 @@
    8.78                  Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
    8.79  
    8.80    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
    8.81 -(*+isa==isa2*)ist''' |> Istate.string_of;
    8.82 +(*+isa==isa2*)ist''' |> Istate.string_of ctxt;
    8.83  
    8.84  "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
    8.85    = (prog ,(pt, (lev_dn p, Res)), is, ctxt);
    8.86 @@ -154,7 +154,7 @@
    8.87  
    8.88  (*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term);
    8.89    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
    8.90 -(*+isa==isa2*)(Pstate iii |> Istate.string_of);
    8.91 +(*+isa==isa2*)(Pstate iii |> Istate.string_of ctxt);
    8.92  
    8.93  "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
    8.94    = ((prog, (ptp, ctxt)), (Pstate ist));
    8.95 @@ -169,7 +169,7 @@
    8.96    = (cc ,(ist |> path_down [L, R]), e);
    8.97  
    8.98    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
    8.99 -(*+isa==isa2*)(Pstate ist |> Istate.string_of);
   8.100 +(*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt);
   8.101  
   8.102      (*if*) Tactical.contained_in t (*else*);
   8.103  
   8.104 @@ -208,13 +208,13 @@
   8.105      check_tac cc ist (prog_tac, form_arg)
   8.106  
   8.107    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
   8.108 -(*+isa==isa2*)(Pstate ist |> Istate.string_of);
   8.109 +(*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt);
   8.110  
   8.111  "~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";
   8.112         val (Accept_Tac (tac, ist, ctxt)) = return;
   8.113  
   8.114    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
   8.115 -(*+isa==isa2*)(Pstate ist |> Istate.string_of)
   8.116 +(*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt)
   8.117  
   8.118  val return =
   8.119        Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);
   8.120 @@ -227,13 +227,13 @@
   8.121  (*+isa==isa2*)pos; (*from check_tac*)
   8.122  (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];
   8.123    val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
   8.124 -(*+isa==isa2*)is1 |> Istate.string_of;
   8.125 +(*+isa==isa2*)is1 |> Istate.string_of ctxt;
   8.126    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
   8.127 -(*+isa==isa2*)(ist' |> Istate.string_of)
   8.128 +(*+isa==isa2*)(ist' |> Istate.string_of ctxt)
   8.129  (*-------------------- stop step into me Apply_Method ----------------------------------------*)
   8.130  (*+isa==isa2*)val "c_2 = 0" = f2str f;
   8.131    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
   8.132 -(*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of)
   8.133 +(*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of ctxt)
   8.134  (*\\------------------- step into me Apply_Method ------------------------------------------//*)
   8.135  
   8.136  val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f;
   8.137 @@ -244,9 +244,9 @@
   8.138                         Substitute ["c_2 = 0"](**) = nxt'''';
   8.139  (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');
   8.140    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
   8.141 -(*+isa==isa2*)is1 |> Istate.string_of;
   8.142 +(*+isa==isa2*)is1 |> Istate.string_of ctxt;
   8.143    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
   8.144 -(*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of;
   8.145 +(*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of ctxt;
   8.146  
   8.147  (*//------------------ step into me Take ---------------------------------------------------\\*)
   8.148  "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
   8.149 @@ -258,7 +258,7 @@
   8.150    		    ("ok", (_, _, ptp)) => ptp;
   8.151  
   8.152    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
   8.153 -(*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of;
   8.154 +(*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of ctxt;
   8.155  
   8.156      (*case*)
   8.157        Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
   8.158 @@ -280,7 +280,7 @@
   8.159  	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
   8.160  
   8.161    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
   8.162 -(*+isa==isa2*)ist |> Istate.string_of;
   8.163 +(*+isa==isa2*)ist |> Istate.string_of ctxt;
   8.164  
   8.165          (*case*)
   8.166          LI.find_next_step sc (pt, pos) ist ctxt (*of*);
   8.167 @@ -297,7 +297,7 @@
   8.168    = ((prog, cc), (trans_scan_up ist));
   8.169  
   8.170    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, false)" =
   8.171 -(*+isa==isa2*)Pstate ist |> Istate.string_of;
   8.172 +(*+isa==isa2*)Pstate ist |> Istate.string_of ctxt;
   8.173  (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term;
   8.174  
   8.175      (*if*) path = [R] (*root of the program body*) (*else*);
   8.176 @@ -376,7 +376,7 @@
   8.177               "[c = L * q_0 / 2, c_2 = 0]"(**) = f2str f;
   8.178  (*val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =*)
   8.179    val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =
   8.180 -(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of);
   8.181 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
   8.182  
   8.183  case nxt of
   8.184      (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()

     9.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Mon Jan 09 16:40:54 2023 +0100
     9.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Tue Jan 10 10:01:05 2023 +0100
     9.3 @@ -242,13 +242,13 @@
     9.4  (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
     9.5  (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*)
     9.6  
     9.7 -(*+*)if (get_istate_LI pt p |> Istate.string_of) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
     9.8 +(*+*)if (get_istate_LI pt p |> Istate.string_of ctxt) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
     9.9  (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
    9.10  (*+*)then () else error "rat-eq + subpbl: istate in specify-phase";
    9.11  
    9.12  (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)
    9.13  
    9.14 -(*+*)if (get_istate_LI pt p |> Istate.string_of) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
    9.15 +(*+*)if (get_istate_LI pt p |> Istate.string_of ctxt) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
    9.16  (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\", \"\n(v_v, x)\"], [R, L, R, L, L, R, R, R], empty, SOME e_e, \n5 * x / (x + - 1 * 2) + - 1 * x / (x + 2) = 4, ORundef, true, true)"
    9.17  (*+*)then () else error "rat-eq + subpbl: istate after found_accept";
    9.18  

    10.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml	Mon Jan 09 16:40:54 2023 +0100
    10.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml	Tue Jan 10 10:01:05 2023 +0100
    10.3 @@ -102,7 +102,7 @@
    10.4          val thy' = get_obj g_domID pt (par_pblobj pt p);
    10.5  	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
    10.6  
    10.7 -(*+*)Istate.string_of ist
    10.8 +(*+*)Istate.string_of ctxt ist
    10.9   = "Pstate ([\"\n(e_e, - 1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], empty, NONE, \n[x = 1],"
   10.10    ^ " ORundef, true, false)"; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~true ok*)
   10.11  

    11.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Mon Jan 09 16:40:54 2023 +0100
    11.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Tue Jan 10 10:01:05 2023 +0100
    11.3 @@ -205,7 +205,7 @@
    11.4    andalso
    11.5    (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[precond_rootmet x]"
    11.6    andalso
    11.7 -  Istate.string_of ist_res =
    11.8 +  Istate.string_of ctxt ist_res =
    11.9      "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)"
   11.10  then () else error "/800-append-on-Frm.sml CHANGED";
   11.11