1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Jul 31 12:39:07 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Jul 31 13:23:38 2022 +0200
     1.3 @@ -73,9 +73,9 @@
     1.4    val get_cas: theory -> CAS_Def.T list
     1.5    val add_cas: CAS_Def.T list -> theory -> theory
     1.6    val get_pbls: theory -> Probl_Def.store
     1.7 -  val add_pbls: (Probl_Def.T * References_Def.id) list -> theory -> theory
     1.8 +  val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
     1.9    val get_mets: theory -> Meth_Def.store
    1.10 -  val add_mets: (Meth_Def.T * References_Def.id) list -> theory -> theory
    1.11 +  val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
    1.12    val get_thes: theory -> (Thy_Write.thydata Store.node) list
    1.13    val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.14    val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 
    1.15 @@ -121,12 +121,13 @@
    1.16      val merge = Store.merge;
    1.17      );
    1.18    fun get_pbls thy = Data.get thy;
    1.19 -  fun add_pbls pbts thy = let
    1.20 -          fun add_pbt (pbt as {guh,...}, pblID) =
    1.21 -                (* the pblID has the leaf-element as first; better readability achieved *)
    1.22 -                (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
    1.23 -                  rev pblID |> Store.insert pblID pbt);
    1.24 -        in Data.map (fold add_pbt pbts) thy end;
    1.25 +  fun add_pbls ctxt pbts thy =
    1.26 +    let
    1.27 +      fun add_pbt (pbt as {guh,...}, pblID) =
    1.28 +        (* the pblID has the leaf-element as first; better readability achieved *)
    1.29 +        (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
    1.30 +          rev pblID |> Store.insert pblID pbt);
    1.31 +    in Data.map (fold add_pbt pbts) thy end;
    1.32  
    1.33    structure Data = Theory_Data (
    1.34      type T = Meth_Def.store;
    1.35 @@ -135,11 +136,12 @@
    1.36      val merge = Store.merge;
    1.37      );
    1.38    val get_mets = Data.get;
    1.39 -  fun add_mets mets thy = let
    1.40 -          fun add_met (met as {guh,...}, metID) =
    1.41 -                (if (!Check_Unique.on) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.42 -                  Store.insert metID met metID);
    1.43 -        in Data.map (fold add_met mets) thy end;
    1.44 +  fun add_mets ctxt mets thy =
    1.45 +    let
    1.46 +      fun add_met (met as {guh,...}, metID) =
    1.47 +        (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
    1.48 +          Store.insert metID met metID);
    1.49 +    in Data.map (fold add_met mets) thy end;
    1.50  
    1.51    structure Data = Theory_Data (
    1.52      type T = (Thy_Write.thydata Store.node) list;

     2.1 --- a/src/Tools/isac/BaseDefinitions/check-unique.sml	Sun Jul 31 12:39:07 2022 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/check-unique.sml	Sun Jul 31 13:23:38 2022 +0200
     2.3 @@ -3,18 +3,21 @@
     2.4     (c) due to copyright terms
     2.5  
     2.6  Check entries to Know_Store unique.
     2.7 -This is legacy code; check runs on #guh.
     2.8 +This is legacy code; check runs on #guh using check_unique
     2.9  
    2.10  "guh" stands for "globally unique handle" -- over all of the internet,
    2.11  the last remaining code from Klaus Schmaranz's Dinopolis Project.
    2.12  *)
    2.13 +
    2.14 +(* switch for checking guhs unique before storing a pbl or met;
    2.15 +   set true at startup (done at begin of ROOT.ML)
    2.16 +   set false for editing Isac_Knowledge (done at end of ROOT.ML).
    2.17 +   Must be global for re-use in other structs *)
    2.18 +val check_unique = Attrib.setup_config_bool \<^binding>\<open>check_unique\<close> (K true);
    2.19 +
    2.20  signature CHECK_UNIQUE =
    2.21  sig
    2.22 -(*type guh *)
    2.23    type id
    2.24 -(*val check_guhs_unique *)
    2.25 -  val on: bool Unsynchronized.ref
    2.26 -(*val collect *)
    2.27    val collect: ('a -> 'b) -> 'a Store.T -> 'b list;
    2.28    val message: ('a -> id list) -> id -> 'a -> unit;
    2.29  end
    2.30 @@ -26,10 +29,7 @@
    2.31  
    2.32  type id = string;
    2.33  
    2.34 -(* switch for checking guhs unique before storing a pbl or met;
    2.35 -   set true at startup (done at begin of ROOT.ML)
    2.36 -   set false for editing Isac_Knowledge (done at end of ROOT.ML) *)
    2.37 -val on = Unsynchronized.ref true;
    2.38 +(*val on = Unsynchronized.ref true;*)
    2.39  
    2.40  fun collect select_guh pbls =
    2.41    let
    2.42 @@ -43,7 +43,7 @@
    2.43    if member op = (select store) id
    2.44    then raise ERROR ("Check_Unique failed with \"" ^ id ^ "\";\n" ^
    2.45  	      "use \"sort_guhs()\" for a list of guhs;\n" ^
    2.46 -	      "consider setting \"Check_Unique.on := false\"")
    2.47 +	      "consider setting \"Config.put check_unique false @{context}\"")
    2.48    else ();
    2.49  
    2.50  (**)end(**)

     3.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Jul 31 12:39:07 2022 +0200
     3.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Jul 31 13:23:38 2022 +0200
     3.3 @@ -187,7 +187,7 @@
     3.4  ML \<open>@{thm last_thmI}\<close>
     3.5  (** )ML \<open>@{thm Querkraft_Belastung}\<close>( *exception FAIL NONE raised (line 161 of "General/scan.ML")*)
     3.6  
     3.7 -ML \<open>Check_Unique.on := false;\<close>
     3.8 +declare [[check_unique = false]]
     3.9  ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
    3.10  ML \<open>@{theory "Isac_Knowledge"}\<close>
    3.11  ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]

     4.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Sun Jul 31 12:39:07 2022 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Sun Jul 31 13:23:38 2022 +0200
     4.3 @@ -137,7 +137,7 @@
     4.4  subsection \<open>Add error patterns\<close>
     4.5  subsubsection \<open>Error patterns for differentiation\<close>
     4.6  
     4.7 -setup \<open>KEStore_Elems.add_mets
     4.8 +setup \<open>KEStore_Elems.add_mets @{context}
     4.9    [Pbl_Met_Hierarchy.update_metpair @{theory Diff} ["diff", "differentiate_on_R"]
    4.10        [("chain-rule-diff-both",
    4.11          [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
    4.12 @@ -167,7 +167,7 @@
    4.13  
    4.14  subsubsection \<open>Error patterns for calculation with rationals\<close>
    4.15  
    4.16 -setup \<open>KEStore_Elems.add_mets
    4.17 +setup \<open>KEStore_Elems.add_mets @{context}
    4.18    [Pbl_Met_Hierarchy.update_metpair @{theory Rational} ["simplification", "of_rationals"]
    4.19        [("addition-of-fractions",
    4.20          [TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",

     5.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sun Jul 31 12:39:07 2022 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sun Jul 31 13:23:38 2022 +0200
     5.3 @@ -141,9 +141,8 @@
     5.4  consts
     5.5    decomposedFunction :: "real => una"
     5.6  
     5.7 -ML \<open>
     5.8 -Check_Unique.on := false; (*WN120307 REMOVE after editing*)
     5.9 -\<close>
    5.10 +declare [[check_unique = false]] (*WN120307 REMOVE after editing*)
    5.11 +
    5.12  problem pbl_simp_rat_partfrac : "partial_fraction/rational/simplification" =
    5.13    \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_ TODO*)]\<close>
    5.14    Method_Ref: "simplification/of_rationals/to_partial_fraction"

     6.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Sun Jul 31 12:39:07 2022 +0200
     6.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Sun Jul 31 13:23:38 2022 +0200
     6.3 @@ -136,7 +136,7 @@
     6.4                NONE => @{thm refl}
     6.5              | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
     6.6            val arg = prep_input thy name maa id_empty (metID, model_input, input, thm);
     6.7 -        in KEStore_Elems.add_mets [arg] thy end)))
     6.8 +        in KEStore_Elems.add_mets @{context} [arg] thy end)))
     6.9  
    6.10  in end;
    6.11  

     7.1 --- a/src/Tools/isac/MathEngBasic/problem.sml	Sun Jul 31 12:39:07 2022 +0200
     7.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml	Sun Jul 31 13:23:38 2022 +0200
     7.3 @@ -270,7 +270,7 @@
     7.4               * in case there are no errors, do prep_input_PIDE (to be simplified)
     7.5               *)
     7.6              val arg = prep_input_PIDE thy name maa id_empty (pblID, model_input, input, cas, metIDs);
     7.7 -          in KEStore_Elems.add_pbls [arg] thy end)))
     7.8 +          in KEStore_Elems.add_pbls @{context} [arg] thy end)))
     7.9  
    7.10  in end;
    7.11  

     8.1 --- a/test/Tools/isac/Knowledge/integrate.thy	Sun Jul 31 12:39:07 2022 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/integrate.thy	Sun Jul 31 13:23:38 2022 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4    (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'') #>
     8.5      (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'')         #>
     8.6      (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
     8.7 -setup \<open>KEStore_Elems.add_mets
     8.8 +setup \<open>KEStore_Elems.add_mets @{context}
     8.9    [MethodC.prep_input @{theory "Isac_Knowledge"} "met_testint" [] MethodC.id_empty
    8.10  	    (["diff", "integration", "test"],
    8.11  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],

     9.1 --- a/test/Tools/isac/ProgLang/calculate.thy	Sun Jul 31 12:39:07 2022 +0200
     9.2 +++ b/test/Tools/isac/ProgLang/calculate.thy	Sun Jul 31 13:23:38 2022 +0200
     9.3 @@ -17,7 +17,7 @@
     9.4  "-calculate.thy: provides 'setup' -----------------------";
     9.5  \<close>
     9.6  
     9.7 -setup \<open>KEStore_Elems.add_pbls
     9.8 +setup \<open>KEStore_Elems.add_pbls @{context}
     9.9    [Problem.prep_input @{theory "Test"} "pbl_ttest" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, []),
    9.10      Problem.prep_input @{theory "Test"} "pbl_ttest_calc" [] Problem.id_empty
    9.11        (["calculate", "test"],
    9.12 @@ -33,7 +33,7 @@
    9.13       (Try (Repeat (Calculate ''TIMES''))) #>
    9.14       (Try (Repeat (Calculate ''DIVIDE''))) #>
    9.15       (Try (Repeat (Calculate ''POWER''))))) t_t"
    9.16 -setup \<open>KEStore_Elems.add_mets
    9.17 +setup \<open>KEStore_Elems.add_mets @{context}
    9.18    [MethodC.prep_input (@{theory "Test"}) "met_testcal" [] MethodC.id_empty
    9.19        (["Test", "test_calculate"],
    9.20          [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],

    10.1 --- a/test/Tools/isac/Specify/refine.thy	Sun Jul 31 12:39:07 2022 +0200
    10.2 +++ b/test/Tools/isac/Specify/refine.thy	Sun Jul 31 13:23:38 2022 +0200
    10.3 @@ -13,7 +13,7 @@
    10.4  \<close>
    10.5  
    10.6  section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
    10.7 -setup \<open>KEStore_Elems.add_pbls
    10.8 +setup \<open>KEStore_Elems.add_pbls @{context}
    10.9  [(Problem.prep_input @{theory} "pbl_test_refine" [] Problem.id_empty
   10.10    (["refine", "test"], [], Rule_Set.empty, NONE, [])),
   10.11  (Problem.prep_input @{theory Diff_App} "pbl_pbla" [] Problem.id_empty