turned simp_trace_depth_limit into a configuration option

--- a/src/Pure/Isar/attrib.ML	Wed Dec 15 19:15:06 2010 -0800
+++ b/src/Pure/Isar/attrib.ML	Thu Dec 16 09:10:38 2010 +0100
@@ -416,6 +416,7 @@
   register_config Unify.trace_simp_raw #>
   register_config Unify.trace_types_raw #>
   register_config MetaSimplifier.simp_depth_limit_raw #>
+  register_config MetaSimplifier.simp_trace_depth_limit_raw #>
   register_config MetaSimplifier.simp_debug_raw #>
   register_config MetaSimplifier.simp_trace_raw));
 

--- a/src/Pure/ProofGeneral/preferences.ML	Wed Dec 15 19:15:06 2010 -0800
+++ b/src/Pure/ProofGeneral/preferences.ML	Thu Dec 16 09:10:38 2010 +0100
@@ -150,7 +150,7 @@
  [bool_pref simp_trace_default
     "trace-simplifier"
     "Trace simplification rules.",
-  nat_pref simp_trace_depth_limit
+  nat_pref simp_trace_depth_limit_default
     "trace-simplifier-depth"
     "Trace simplifier depth limit.",
   bool_pref trace_rules

--- a/src/Pure/meta_simplifier.ML	Wed Dec 15 19:15:06 2010 -0800
+++ b/src/Pure/meta_simplifier.ML	Thu Dec 16 09:10:38 2010 +0100
@@ -16,7 +16,9 @@
   val simp_trace: bool Config.T
   val simp_trace_raw: Config.raw
   val simp_trace_default: bool Unsynchronized.ref
-  val simp_trace_depth_limit: int Unsynchronized.ref
+  val simp_trace_depth_limit: int Config.T
+  val simp_trace_depth_limit_raw: Config.raw
+  val simp_trace_depth_limit_default: int Unsynchronized.ref
   type rrule
   val eq_rrule: rrule * rrule -> bool
   type simpset
@@ -253,10 +255,16 @@
 val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
 val simp_depth_limit = Config.int simp_depth_limit_raw;
 
-val simp_trace_depth_limit = Unsynchronized.ref 1;
+val simp_trace_depth_limit_default = Unsynchronized.ref 1;
+val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
+  (fn _ => Config.Int (! simp_trace_depth_limit_default));
+val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
 
-fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
-  if depth > ! simp_trace_depth_limit then
+fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default
+  | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit;
+
+fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg =
+  if depth > simp_trace_depth_limit_of context then
     if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
   else
     (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
@@ -264,7 +272,7 @@
 val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
   (rules, prems, bounds,
     (depth + 1,
-      if depth = ! simp_trace_depth_limit then Unsynchronized.ref false else exceeded), context));
+      if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
 
 fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;