1.1 --- a/src/Tools/isac/Interpret/derive.sml	Sat Jul 30 16:47:45 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Sun Jul 31 12:39:07 2022 +0200
     1.3 @@ -47,8 +47,8 @@
     1.4  
     1.5  (** make one triple towards the goal term **)
     1.6  
     1.7 -fun msg_1 rts =
     1.8 -  (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");
     1.9 +fun msg_1 ctxt rts =
    1.10 +  (tracing ("do_one exceeds " ^ int2str (Config.get ctxt rewrite_limit) ^ "with derivation =\n");
    1.11     tracing (deriv2str rts));
    1.12  fun msg_2 ctxt thmid =
    1.13    if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
    1.14 @@ -73,7 +73,7 @@
    1.15          | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
    1.16      and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
    1.17        if lim < 0 
    1.18 -      then (msg_1 rts; rts)
    1.19 +      then (msg_1 ctxt rts; rts)
    1.20        else
    1.21          (case r of
    1.22            Rule.Thm (thmid, tm) => 
    1.23 @@ -101,7 +101,7 @@
    1.24            | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
    1.25          | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
    1.26      | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
    1.27 -  in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
    1.28 +  in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end
    1.29  
    1.30  
    1.31  (** concatenate several steps in revers order **)

     2.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Sat Jul 30 16:47:45 2022 +0200
     2.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Jul 31 12:39:07 2022 +0200
     2.3 @@ -21,9 +21,6 @@
     2.4    val rewrite_terms_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
     2.5      -> term -> (term * term list) option
     2.6  
     2.7 -  val depth: int Unsynchronized.ref
     2.8 -  val lim_deriv: int Unsynchronized.ref
     2.9 -
    2.10  \<^isac_test>\<open>
    2.11    val rewrite__: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ ->
    2.12      Rule_Set.T -> bool -> thm -> term -> (term * term list) option
    2.13 @@ -43,6 +40,9 @@
    2.14  
    2.15  (* must be global for re-use in other structs *)
    2.16  val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
    2.17 +(* no of rewrites exceeding this int -> NO_REWRITE *)
    2.18 +val rewrite_limit = Attrib.setup_config_int \<^binding>\<open>rewrite_limit\<close> (K 100);
    2.19 +
    2.20  (**)
    2.21  structure Rewrite(**): REWRITE(**) =
    2.22  struct
    2.23 @@ -51,19 +51,19 @@
    2.24  exception NO_REWRITE;
    2.25  
    2.26  (* depth of recursion in traces of the rewriter, if trace_on:=true *)
    2.27 -val depth = Unsynchronized.ref 99999;
    2.28 -(* no of rewrites exceeding this int -> NO rewrite *)
    2.29 -val lim_deriv = Unsynchronized.ref 100;
    2.30 +val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999);
    2.31  
    2.32  fun trace ctxt i str = 
    2.33 -  if Config.get ctxt rewrite_trace andalso i < ! depth then tracing (idt "#" i ^ str) else ()
    2.34 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
    2.35 +  then tracing (idt "#" i ^ str) else ()
    2.36  fun trace_eq1 ctxt i str rrls t =
    2.37    trace ctxt i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_ctxt ctxt t)
    2.38  fun trace_eq2 ctxt i str t t' =
    2.39    trace ctxt i (" " ^ str ^ ": \"" ^
    2.40      UnparseC.term_in_ctxt ctxt t ^ "\" > \"" ^ UnparseC.term_in_ctxt ctxt t' ^ "\"");
    2.41  fun trace1 ctxt i str =
    2.42 -  if Config.get ctxt rewrite_trace andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
    2.43 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
    2.44 +  then tracing (idt "#" (i + 1) ^ str) else ()
    2.45  fun trace_in1 ctxt i str thmid =
    2.46    trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
    2.47  fun trace_in2 ctxt i str t =
    2.48 @@ -71,12 +71,12 @@
    2.49  fun trace_in3 ctxt i str pairopt =
    2.50    trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt));
    2.51  fun trace_in4 ctxt i str ts ts' =
    2.52 -  if Config.get ctxt rewrite_trace andalso i < ! depth andalso ts <> []
    2.53 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth andalso ts <> []
    2.54    then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt ts ^
    2.55    	"   stored: " ^ UnparseC.terms_in_ctxt ctxt ts')
    2.56    else ();
    2.57  fun trace_in5 ctxt i str p' =
    2.58 -  if Config.get ctxt rewrite_trace andalso i < ! depth 
    2.59 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
    2.60    then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt p')
    2.61    else();
    2.62  fun msg call ctxt op_ thmC t = 

     3.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Sat Jul 30 16:47:45 2022 +0200
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Sun Jul 31 12:39:07 2022 +0200
     3.3 @@ -43,11 +43,11 @@
     3.4  ML \<open>
     3.5  val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)";
     3.6  
     3.7 -val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
     3.8 -val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; UnparseC.term t;
     3.9 -val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_pow t; UnparseC.term t;
    3.10 -val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_var t; UnparseC.term t;
    3.11 -val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_const t; UnparseC.term t;
    3.12 +val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
    3.13 +val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
    3.14 +val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_pow t; UnparseC.term t;
    3.15 +val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_var t; UnparseC.term t;
    3.16 +val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t; UnparseC.term t;
    3.17  \<close>
    3.18  text \<open>Please, scoll up the Output-window to check the 5 steps of rewriting !
    3.19    You might not be satisfied by the result "2 * x \<up> (2 - 1) + 1 + 0".
    3.20 @@ -55,8 +55,7 @@
    3.21    ISAC has a set of rules called 'make_polynomial', which simplifies the result:
    3.22  \<close>
    3.23  ML \<open>
    3.24 -val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t;
    3.25 -Rewrite.trace_on := false; (*true false*)
    3.26 +val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t; UnparseC.term t;
    3.27  \<close>
    3.28  
    3.29  section \<open>Note on bound variables\<close>
    3.30 @@ -158,11 +157,9 @@
    3.31  text \<open>The simplifiers are quite busy when finding the above results. you can
    3.32    watch them at work by setting the switch 'Rewrite.trace_on:\<close>
    3.33  ML \<open>
    3.34 -Rewrite.trace_on := false; (*true false*)
    3.35  tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
    3.36  val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t;
    3.37  tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
    3.38 -Rewrite.trace_on := false; (*true false*)
    3.39  \<close>
    3.40  text \<open>You see what happend when you click the checkbox <Tracing> on the bar
    3.41    separating this window from the Output-window.