1.1 --- a/src/Tools/isac/BaseDefinitions/check-unique.sml	Sun Jul 31 13:23:38 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/check-unique.sml	Sun Jul 31 13:45:20 2022 +0200
     1.3 @@ -29,8 +29,6 @@
     1.4  
     1.5  type id = string;
     1.6  
     1.7 -(*val on = Unsynchronized.ref true;*)
     1.8 -
     1.9  fun collect select_guh pbls =
    1.10    let
    1.11      fun node coll (Store.Node (_, [n], ns)) = [select_guh n] @ (nodes coll ns)

     2.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Jul 31 13:23:38 2022 +0200
     2.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Jul 31 13:45:20 2022 +0200
     2.3 @@ -202,14 +202,6 @@
     2.4  text \<open>
     2.5    REPLACE BY Know_Store... (has been overlooked)
     2.6      calcelems.sml:val rew_ord' = Unsynchronized.ref ...
     2.7 -  KEEP FOR TRACING
     2.8 -    rewrite.sml:val Rewrite.trace_on = Unsynchronized.ref false;
     2.9 -    rewrite.sml:val depth = Unsynchronized.ref 99999;
    2.10 -    rewrite.sml:val lim_rewrite = Unsynchronized.ref 99999;
    2.11 -    rewrite.sml:val lim_deriv = Unsynchronized.ref 100;
    2.12 -    Interpret/rewtools.sml:val LItool.trace = Unsynchronized.ref false;
    2.13 -  KEEP FOR EASIER DEVELOPMENT
    2.14 -    calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
    2.15    KEEP FOR DEMOS
    2.16      Knowledge/GCD_Poly_ML.thy:  val trace_div = Unsynchronized.ref true;
    2.17      Knowledge/GCD_Poly_ML.thy:  val trace_div_invariant = Unsynchronized.ref false;

     3.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sun Jul 31 13:23:38 2022 +0200
     3.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sun Jul 31 13:45:20 2022 +0200
     3.3 @@ -25,7 +25,6 @@
     3.4    val get_simplifier: Calc.T -> Rule_Set.T
     3.5    val tac_from_prog: Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
     3.6  
     3.7 -  val trace_on: bool Unsynchronized.ref
     3.8  \<^isac_test>\<open>
     3.9    val arguments_from_model : MethodC.id -> I_Model.T -> term list
    3.10  \<close>
    3.11 @@ -39,7 +38,7 @@
    3.12  open Pos
    3.13  
    3.14  (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)   
    3.15 -val trace_on = Unsynchronized.ref false; (* TODO: adopt Isabelle's tracing *)
    3.16 +val LI_trace = Attrib.setup_config_bool \<^binding>\<open>LI_trace\<close> (K false);
    3.17  
    3.18  (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
    3.19  fun implicit_take (Rule.Prog prog) env =
    3.20 @@ -104,8 +103,8 @@
    3.21    thus it does ContextC.insert_assumptions in case of Rewrite*.
    3.22    The argument Ctree.ctree is required only for Subproblem'.
    3.23  *)
    3.24 -fun trace_msg_3 tac =
    3.25 -  if (!trace_on) then
    3.26 +fun trace_msg_3 ctxt tac =
    3.27 +  if Config.get ctxt LI_trace then
    3.28      tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
    3.29        "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
    3.30    else ();
    3.31 @@ -200,8 +199,8 @@
    3.32          (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
    3.33            if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated
    3.34        | _ => raise ERROR ("associate: uncovered case"))
    3.35 -  | associate _ _ (tac, _) = 
    3.36 -    (trace_msg_3 tac; Not_Associated);
    3.37 +  | associate _ ctxt (tac, _) = 
    3.38 +    (trace_msg_3 ctxt tac; Not_Associated);
    3.39  
    3.40  (* create the initial interpreter state
    3.41    from the items of the guard and the formal arguments of the program.
    3.42 @@ -245,8 +244,8 @@
    3.43  	"with\n" ^
    3.44  	"formals: " ^ UnparseC.terms formals ^ "\n" ^
    3.45  	"actuals: " ^ UnparseC.terms actuals
    3.46 -fun trace_init metID =
    3.47 -  if (!trace_on) 
    3.48 +fun trace_init ctxt metID =
    3.49 +  if Config.get ctxt LI_trace
    3.50    then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
    3.51    else ();
    3.52  in
    3.53 @@ -255,7 +254,7 @@
    3.54      val actuals = arguments_from_model metID itms
    3.55      val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
    3.56      val (scr, sc) = (case (#scr o MethodC.from_store) metID of
    3.57 -           scr as Rule.Prog sc => (trace_init metID; (scr, sc))
    3.58 +           scr as Rule.Prog sc => (trace_init ctxt metID; (scr, sc))
    3.59         | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string metID))
    3.60      val formals = Program.formal_args sc    
    3.61      fun assoc_by_type f aa =
    3.62 @@ -312,12 +311,12 @@
    3.63    end
    3.64  
    3.65  
    3.66 -fun trace_msg_1 call t stac =
    3.67 -  if (! trace_on) then
    3.68 +fun trace_msg_1 ctxt call t stac =
    3.69 +  if Config.get ctxt LI_trace then
    3.70  	  tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term t ^ "\" \<longrightarrow> Tac \"" ^ UnparseC.term stac ^ "\"")
    3.71  	else ();
    3.72 -fun trace_msg_2 call t lexpr' =
    3.73 -  if (! trace_on) then
    3.74 +fun trace_msg_2 ctxt call t lexpr' =
    3.75 +  if Config.get ctxt LI_trace then
    3.76  	  tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \<longrightarrow> Expr \"" ^ UnparseC.term lexpr' ^ "\"")
    3.77  	else ();
    3.78  (*
    3.79 @@ -331,14 +330,14 @@
    3.80  	        val stac' = Rewrite.eval_prog_expr ctxt srls 
    3.81                (subst_atomic (Env.update_opt E (a, v)) stac)
    3.82  	      in
    3.83 -          (trace_msg_1 call t stac; (Program.Tac stac', a'))
    3.84 +          (trace_msg_1 ctxt call t stac; (Program.Tac stac', a'))
    3.85  	      end
    3.86      | (Program.Expr lexpr, a') =>
    3.87  	      let
    3.88  	        val lexpr' = Rewrite.eval_prog_expr ctxt srls
    3.89                (subst_atomic (Env.update_opt E (a, v)) lexpr)
    3.90  	      in
    3.91 -          (trace_msg_2 call t lexpr'; (Program.Expr lexpr', a'))
    3.92 +          (trace_msg_2 ctxt call t lexpr'; (Program.Expr lexpr', a'))
    3.93  	      end;
    3.94  
    3.95  (**)end(**)