1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Sat Jul 30 16:47:45 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Jul 31 12:39:07 2022 +0200
     1.3 @@ -21,9 +21,6 @@
     1.4    val rewrite_terms_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
     1.5      -> term -> (term * term list) option
     1.6  
     1.7 -  val depth: int Unsynchronized.ref
     1.8 -  val lim_deriv: int Unsynchronized.ref
     1.9 -
    1.10  \<^isac_test>\<open>
    1.11    val rewrite__: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ ->
    1.12      Rule_Set.T -> bool -> thm -> term -> (term * term list) option
    1.13 @@ -43,6 +40,9 @@
    1.14  
    1.15  (* must be global for re-use in other structs *)
    1.16  val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
    1.17 +(* no of rewrites exceeding this int -> NO_REWRITE *)
    1.18 +val rewrite_limit = Attrib.setup_config_int \<^binding>\<open>rewrite_limit\<close> (K 100);
    1.19 +
    1.20  (**)
    1.21  structure Rewrite(**): REWRITE(**) =
    1.22  struct
    1.23 @@ -51,19 +51,19 @@
    1.24  exception NO_REWRITE;
    1.25  
    1.26  (* depth of recursion in traces of the rewriter, if trace_on:=true *)
    1.27 -val depth = Unsynchronized.ref 99999;
    1.28 -(* no of rewrites exceeding this int -> NO rewrite *)
    1.29 -val lim_deriv = Unsynchronized.ref 100;
    1.30 +val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999);
    1.31  
    1.32  fun trace ctxt i str = 
    1.33 -  if Config.get ctxt rewrite_trace andalso i < ! depth then tracing (idt "#" i ^ str) else ()
    1.34 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
    1.35 +  then tracing (idt "#" i ^ str) else ()
    1.36  fun trace_eq1 ctxt i str rrls t =
    1.37    trace ctxt i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_ctxt ctxt t)
    1.38  fun trace_eq2 ctxt i str t t' =
    1.39    trace ctxt i (" " ^ str ^ ": \"" ^
    1.40      UnparseC.term_in_ctxt ctxt t ^ "\" > \"" ^ UnparseC.term_in_ctxt ctxt t' ^ "\"");
    1.41  fun trace1 ctxt i str =
    1.42 -  if Config.get ctxt rewrite_trace andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
    1.43 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
    1.44 +  then tracing (idt "#" (i + 1) ^ str) else ()
    1.45  fun trace_in1 ctxt i str thmid =
    1.46    trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
    1.47  fun trace_in2 ctxt i str t =
    1.48 @@ -71,12 +71,12 @@
    1.49  fun trace_in3 ctxt i str pairopt =
    1.50    trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt));
    1.51  fun trace_in4 ctxt i str ts ts' =
    1.52 -  if Config.get ctxt rewrite_trace andalso i < ! depth andalso ts <> []
    1.53 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth andalso ts <> []
    1.54    then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt ts ^
    1.55    	"   stored: " ^ UnparseC.terms_in_ctxt ctxt ts')
    1.56    else ();
    1.57  fun trace_in5 ctxt i str p' =
    1.58 -  if Config.get ctxt rewrite_trace andalso i < ! depth 
    1.59 +  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
    1.60    then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt p')
    1.61    else();
    1.62  fun msg call ctxt op_ thmC t =