# HG changeset patch # User nipkow # Date 1136389120 -3600 # Node ID 0ee7eab8c845bfb35e13ed5e4073da7441626833 # Parent dab1dd61e59da2b341db12390d671b6f26763648 trace_simp_depth_limit is 1 by default diff -r dab1dd61e59d -r 0ee7eab8c845 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Wed Jan 04 16:37:57 2006 +0100 +++ b/src/Pure/meta_simplifier.ML Wed Jan 04 16:38:40 2006 +0100 @@ -241,13 +241,17 @@ val trace_simp = ref false; val simp_depth = ref 0; val simp_depth_limit = ref 100; -val trace_simp_depth_limit = ref 100; - +val trace_simp_depth_limit = ref 1; +val trace_simp_depth_limit_exceeded = ref false; local fun println a = - if ! simp_depth > ! trace_simp_depth_limit then () - else tracing (enclose "[" "]" (string_of_int (! simp_depth)) ^ a); + if ! simp_depth > ! trace_simp_depth_limit + then if !trace_simp_depth_limit_exceeded then () + else (tracing "trace_simp_depth_limit exceeded!"; + trace_simp_depth_limit_exceeded := true) + else (tracing (enclose "[" "]" (string_of_int (! simp_depth)) ^ a); + trace_simp_depth_limit_exceeded := false); fun prnt warn a = if warn then warning a else println a;