1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Jan 11 06:06:12 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Jan 11 09:23:18 2023 +0100
     1.3 @@ -86,7 +86,8 @@
     1.4    val get_ref_last_thy: unit -> theory
     1.5    val set_ref_last_thy: theory -> unit
     1.6    val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy
     1.7 -                                                          * problem refinement                    *)
     1.8 +                                                          * problem refinement                    
     1.9 +                                                          * (test-)code to be deleted            *)
    1.10  end;
    1.11  
    1.12  structure Know_Store(**): KNOW_STORE(**) =

     2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 06:06:12 2023 +0100
     2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 09:23:18 2023 +0100
     2.3 @@ -99,21 +99,24 @@
     2.4    val dest_list': term -> term list
     2.5    val negates: term -> term -> bool
     2.6  
     2.7 -\<^isac_test>\<open>
     2.8 +  val contains_one_of: thm * (string * typ) list -> bool
     2.9 +  val contains_Const_typeless: term list -> term -> bool
    2.10 +  val sym_trm : term -> term (* unused code, kept as hints to design ideas *)
    2.11 +
    2.12 +(*isac_test*)
    2.13    val mk_negative: typ -> term -> term
    2.14 +  val free2var: term -> term
    2.15    val scala_of_term: term -> string
    2.16 -  val atomtyp(*<-- atom_typ TODO*): typ -> unit
    2.17 +
    2.18 +(*val atom_typ: typ -> unit RENAME*)
    2.19 +  val atomtyp: typ -> unit
    2.20    val atomty: term -> unit
    2.21    val atomw: term -> unit
    2.22    val atomt: term -> unit
    2.23    val atomwy: term -> unit
    2.24 -  val atomty_thy: ThyC.id -> term -> unit
    2.25 -  val free2var: term -> term
    2.26 +
    2.27 +\<^isac_test>\<open>
    2.28  \<close>
    2.29 -  val contains_one_of: thm * (string * typ) list -> bool
    2.30 -  val contains_Const_typeless: term list -> term -> bool
    2.31 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    2.32 -  val sym_trm : term -> term
    2.33  end
    2.34  
    2.35  (**)
    2.36 @@ -148,8 +151,7 @@
    2.37      handle Pattern.MATCH => false
    2.38  
    2.39  (** transform  typ / term to a String to be parsed by Scala after transport via libisabelle **)
    2.40 -
    2.41 -\<^isac_test>\<open>
    2.42 +(*isac_test*)
    2.43  fun scala_of_typ (Type (s, typs)) =
    2.44      enclose "Type(" ")" (quote s ^ ", " ^
    2.45        (typs |> map scala_of_typ |> commas |> enclose "List(" ")"))
    2.46 @@ -202,40 +204,28 @@
    2.47    fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***");
    2.48    fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***");
    2.49  end;
    2.50 +
    2.51 +\<^isac_test>\<open>
    2.52  \<close>
    2.53  
    2.54  fun term_detail2str t =
    2.55 -  let 
    2.56 -    fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ T ^ ")"
    2.57 -      | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ T ^ ")"
    2.58 +  let
    2.59 +    val ctxt = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global
    2.60 +    fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    2.61 +      | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    2.62        | ato (Var ((a, i), T)) n =
    2.63 -        "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ T ^ ")"
    2.64 +        "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
    2.65        | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
    2.66        | ato (Abs(a, T, body))  n = 
    2.67 -        "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ T ^ ",.." ^ ato body (n + 1)
    2.68 +        "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1)
    2.69        | ato (f $ t) n = ato f n ^ ato t (n + 1)
    2.70    in "\n*** " ^ ato t 0 ^ "\n***" end;
    2.71  
    2.72 -\<^isac_test>\<open>
    2.73 -fun term_detail2str_thy thy t =
    2.74 -  let
    2.75 -    fun ato (Const (a, T)) n =
    2.76 -        "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")"
    2.77 -  	  | ato (Free (a, T)) n =
    2.78 -  	     "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")"
    2.79 -  	  | ato (Var ((a, i), T)) n =
    2.80 -  	    "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^
    2.81 -  	    UnparseC.typ_by_thyID thy T ^ ")"
    2.82 -  	  | ato (Bound i) n = 
    2.83 -  	    "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
    2.84 -  	  | ato (Abs(a, T, body))  n = 
    2.85 -  	    "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ",.." ^
    2.86 -  	    ato body (n + 1)
    2.87 -  	  | ato (f $ t) n = ato f n ^ ato t (n + 1)
    2.88 -  in "\n*** " ^ ato t 0 ^ "\n***" end;
    2.89 +(*isac_test*)
    2.90  fun atomwy t = (writeln o term_detail2str) t;
    2.91  fun atomty t = (tracing o term_detail2str) t;
    2.92 -fun atomty_thy thy t = (tracing o (term_detail2str_thy thy)) t;
    2.93 +
    2.94 +\<^isac_test>\<open>
    2.95  \<close>
    2.96  
    2.97  (* contains the term a VAR(("*",_),_) ? *)
    2.98 @@ -375,7 +365,7 @@
    2.99    | var2free (Abs(s, T, t)) = Abs(s, T, var2free t)
   2.100    | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
   2.101    
   2.102 -\<^isac_test>\<open>
   2.103 +(*isac_test*)
   2.104  (* Logic.varify does NOT take care of 'Free ("1", _)'*)
   2.105  fun free2var (t as Const _) = t
   2.106    | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T)
   2.107 @@ -383,6 +373,8 @@
   2.108    | free2var (t as Bound _) = t 
   2.109    | free2var (Abs (s, T, t)) = Abs (s, T, free2var t)
   2.110    | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
   2.111 +
   2.112 +\<^isac_test>\<open>
   2.113  \<close>
   2.114  
   2.115  fun mk_listT T = Type (\<^type_name>\<open>list\<close>, [T]);

     3.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml	Wed Jan 11 06:06:12 2023 +0100
     3.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml	Wed Jan 11 09:23:18 2023 +0100
     3.3 @@ -27,12 +27,8 @@
     3.4  
     3.5  (*val terms_short: Proof.context -> term list -> term_as_string*)
     3.6    val terms_short: term list -> term_as_string
     3.7 -
     3.8  (*val typ: Proof.context -> typ -> term_as_string*)
     3.9    val typ_in_ctxt: Proof.context -> typ -> term_as_string
    3.10 -  val typ: typ -> term_as_string
    3.11 -(*replace by ^^^*)
    3.12 -  val typ_by_thyID: ThyC.id -> typ -> term_as_string
    3.13  
    3.14  \<^isac_test>\<open>
    3.15    val term_by_thyID: ThyC.id -> term -> term_as_string
    3.16 @@ -76,16 +72,6 @@
    3.17  fun term_opt (SOME t) = "(SOME " ^ term t ^ ")"
    3.18    | term_opt NONE = "NONE";
    3.19  
    3.20 -fun type_to_string'' (thyID : ThyC.id) t =
    3.21 -  let
    3.22 -    val ctxt' = Config.put show_markup false (Proof_Context.init_global
    3.23 -      (ThyC.get_theory thyID))
    3.24 -  in
    3.25 -    Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t
    3.26 -  end;
    3.27 -fun typ typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
    3.28 -fun typ_by_thyID thy typ = type_to_string'' thy typ; (*legacy*)
    3.29 -
    3.30  fun type_to_string' ctxt typ =
    3.31    Print_Mode.setmp [] (Syntax.string_of_typ ctxt) typ
    3.32  fun typ_in_ctxt ctxt typ = type_to_string' ctxt typ

     4.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Wed Jan 11 06:06:12 2023 +0100
     4.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Wed Jan 11 09:23:18 2023 +0100
     4.3 @@ -159,7 +159,7 @@
     4.4      map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs))
     4.5  fun xml_of_sube sube =
     4.6    XML.Elem (("SUBSTITUTION", []), 
     4.7 -    map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
     4.8 +    map xml_of_sub (Subst.T_from_string_eqs (Know_Store.get_via_last_thy "Isac_Knowledge") sube))
     4.9  
    4.10  fun thm''2xml j (thm : thm) =
    4.11      indt j ^ "<THEOREM>\n" ^

     5.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml	Wed Jan 11 06:06:12 2023 +0100
     5.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml	Wed Jan 11 09:23:18 2023 +0100
     5.3 @@ -76,7 +76,8 @@
     5.4     EXCEPT theory hierarchy ... compare 'fun keref2xml'    *)
     5.5  fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID)
     5.6    handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
     5.7 -fun metID2guh metID = (((#guh o MethodC.from_store ("Isac_Knowledge" |> ThyC.get_theory |> Proof_Context.init_global)) metID)
     5.8 +fun metID2guh metID =
     5.9 +  (((#guh o MethodC.from_store ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global)) metID)
    5.10    handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
    5.11  fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID
    5.12    | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID

     6.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Wed Jan 11 06:06:12 2023 +0100
     6.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Wed Jan 11 09:23:18 2023 +0100
     6.3 @@ -817,7 +817,7 @@
     6.4  
     6.5  (* get the theory explicitly just for the rootpbl;
     6.6     thus use this function _after_ finishing specification *)
     6.7 -fun root_thy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Know_Store.get_via_last_thy thyID
     6.8 +fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory_PIDE ctxt thyID
     6.9    | root_thy _ = raise ERROR "root_thy: uncovered fun def.";
    6.10  
    6.11  (**)

     7.1 --- a/src/Tools/isac/Specify/Specify.thy	Wed Jan 11 06:06:12 2023 +0100
     7.2 +++ b/src/Tools/isac/Specify/Specify.thy	Wed Jan 11 09:23:18 2023 +0100
     7.3 @@ -24,6 +24,7 @@
     7.4  
     7.5  ML \<open>
     7.6  \<close> ML \<open>
     7.7 +ThyC.get_theory_PIDE
     7.8  \<close> ML \<open>
     7.9  \<close> ML \<open>
    7.10  \<close>

     8.1 --- a/src/Tools/isac/Specify/p-spec.sml	Wed Jan 11 06:06:12 2023 +0100
     8.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Wed Jan 11 09:23:18 2023 +0100
     8.3 @@ -176,7 +176,7 @@
     8.4  (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
     8.5  fun unknown_expl dI pbt selcts =
     8.6    let
     8.7 -    val thy = ThyC.get_theory dI
     8.8 +    val thy = Know_Store.get_via_last_thy dI
     8.9      val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
    8.10      val its = O_Model.add_enumerate its_ 
    8.11    in map flattup2 its end

     9.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Jan 11 06:06:12 2023 +0100
     9.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Jan 11 09:23:18 2023 +0100
     9.3 @@ -254,7 +254,7 @@
     9.4    ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
     9.5    ML_file "Minisubpbl/600-postcond.sml"
     9.6    ML_file "Minisubpbl/700-interSteps.sml"
     9.7 -  ML_file "Minisubpbl/710-interSteps-short.sml"  
     9.8 +  ML_file "Minisubpbl/710-interSteps-short.sml"
     9.9    ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
    9.10    ML_file "Minisubpbl/790-complete.sml"
    9.11    ML_file "Minisubpbl/800-append-on-Frm.sml"

    10.1 --- a/test/Tools/isac/Test_Some.thy	Wed Jan 11 06:06:12 2023 +0100
    10.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Jan 11 09:23:18 2023 +0100
    10.3 @@ -120,7 +120,7 @@
    10.4  \<close> ML \<open>
    10.5  \<close>
    10.6  
    10.7 -section \<open>=============="Interpret/error-pattern.sml"========================================\<close>
    10.8 +section \<open>===================================================================================\<close>
    10.9  ML \<open>
   10.10  \<close> ML \<open>
   10.11  \<close> ML \<open>