# HG changeset patch # User boehmes # Date 1292487038 -3600 # Node ID e20f0d0e2af390bffb043433ab6362c96734c135 # Parent 717404c7d59aa9618f7f4ccbe076b9bcfae5e3b0 turned simp_trace_depth_limit into a configuration option diff -r 717404c7d59a -r e20f0d0e2af3 src/Pure/Isar/attrib.ML --- 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)); diff -r 717404c7d59a -r e20f0d0e2af3 src/Pure/ProofGeneral/preferences.ML --- 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 diff -r 717404c7d59a -r e20f0d0e2af3 src/Pure/meta_simplifier.ML --- 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;