1.1 --- a/NEWS	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/NEWS	Sat Mar 27 21:34:28 2010 +0100
     1.3 @@ -68,7 +68,8 @@
     1.4    using [[trace_simp=true]]
     1.5  
     1.6  Tracing is then active for all invocations of the simplifier
     1.7 -in subsequent goal refinement steps.
     1.8 +in subsequent goal refinement steps. Tracing may also still be
     1.9 +enabled or disabled via the ProofGeneral settings menu.
    1.10  
    1.11  
    1.12  *** Pure ***

     2.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Mar 27 18:43:11 2010 +0100
     2.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Mar 27 21:34:28 2010 +0100
     2.3 @@ -146,7 +146,10 @@
     2.4      "Show leading question mark of variable name"];
     2.5  
     2.6  val tracing_preferences =
     2.7 - [nat_pref trace_simp_depth_limit
     2.8 + [bool_pref trace_simp_ref
     2.9 +    "trace-simplifier"
    2.10 +    "Trace simplification rules.",
    2.11 +  nat_pref trace_simp_depth_limit
    2.12      "trace-simplifier-depth"
    2.13      "Trace simplifier depth limit.",
    2.14    bool_pref trace_rules

     3.1 --- a/src/Pure/meta_simplifier.ML	Sat Mar 27 18:43:11 2010 +0100
     3.2 +++ b/src/Pure/meta_simplifier.ML	Sat Mar 27 21:34:28 2010 +0100
     3.3 @@ -15,6 +15,7 @@
     3.4    val debug_simp_value: Config.value Config.T
     3.5    val trace_simp: bool Config.T
     3.6    val trace_simp_value: Config.value Config.T
     3.7 +  val trace_simp_ref: bool Unsynchronized.ref
     3.8    val trace_simp_depth_limit: int Unsynchronized.ref
     3.9    type rrule
    3.10    val eq_rrule: rrule * rrule -> bool
    3.11 @@ -278,6 +279,7 @@
    3.12  
    3.13  val trace_simp_value = Config.declare false "trace_simp" (Config.Bool false);
    3.14  val trace_simp = Config.bool trace_simp_value;
    3.15 +val trace_simp_ref = Unsynchronized.ref false;
    3.16  
    3.17  local
    3.18  
    3.19 @@ -299,25 +301,31 @@
    3.20  fun print_term_global ss warn a thy t =
    3.21    print_term ss warn (K a) t (ProofContext.init thy);
    3.22  
    3.23 -fun if_enabled (Simpset ({context, ...}, _)) flag f =
    3.24 +fun if_enabled (Simpset ({context, ...}, _)) b flag f =
    3.25    (case context of
    3.26 -    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
    3.27 +    SOME ctxt => if b orelse Config.get ctxt flag then f ctxt else ()
    3.28    | NONE => ())
    3.29  
    3.30 -fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
    3.31 -fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
    3.32 +fun debug warn a ss =
    3.33 +  if_enabled ss false debug_simp (fn _ => prnt ss warn (a ()));
    3.34 +fun trace warn a ss =
    3.35 +  if_enabled ss (!trace_simp_ref) trace_simp (fn _ => prnt ss warn (a ()));
    3.36  
    3.37 -fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
    3.38 -fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
    3.39 +fun debug_term warn a ss t =
    3.40 +  if_enabled ss false debug_simp (print_term ss warn a t);
    3.41 +fun trace_term warn a ss t =
    3.42 +  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss warn a t);
    3.43  
    3.44  fun trace_cterm warn a ss ct =
    3.45 -  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
    3.46 +  if_enabled ss (!trace_simp_ref) trace_simp
    3.47 +    (print_term ss warn a (Thm.term_of ct));
    3.48  
    3.49  fun trace_thm a ss th =
    3.50 -  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
    3.51 +  if_enabled ss (!trace_simp_ref) trace_simp
    3.52 +    (print_term ss false a (Thm.full_prop_of th));
    3.53  
    3.54  fun trace_named_thm a ss (th, name) =
    3.55 -  if_enabled ss trace_simp (print_term ss false
    3.56 +  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss false
    3.57      (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
    3.58      (Thm.full_prop_of th));
    3.59