# HG changeset patch
# User blanchet
# Date 1391040235 -3600
# Node ID dc7a6f6be01bc2435a1223d0de0fa1c15931f034
# Parent  cdb9435e3caed0512c099dea181c364274d955b0
systematically suppress tracing if asked for (affects 'meson' proof method)

diff -r cdb9435e3cae -r dc7a6f6be01b src/Pure/search.ML
--- a/src/Pure/search.ML	Thu Jan 30 00:59:12 2014 +0100
+++ b/src/Pure/search.ML	Thu Jan 30 01:03:55 2014 +0100
@@ -124,13 +124,18 @@
      (*bnd = depth bound; inc = estimate of increment required next*)
      fun depth (bnd,inc) [] =
           if bnd > lim then
-             (tracing (string_of_int (!countr) ^
-                       " inferences so far.  Giving up at " ^ string_of_int bnd);
+             (if !trace_DEPTH_FIRST then
+                  tracing (string_of_int (!countr) ^
+                           " inferences so far.  Giving up at " ^
+                           string_of_int bnd)
+              else ();
               NONE)
           else
-             (tracing (string_of_int (!countr) ^
-                       " inferences so far.  Searching to depth " ^
-                       string_of_int bnd);
+             (if !trace_DEPTH_FIRST then
+                  tracing (string_of_int (!countr) ^
+                           " inferences so far.  Searching to depth " ^
+                           string_of_int bnd)
+              else ();
               (*larger increments make it run slower for the hard problems*)
               depth (bnd+inc, 10)) [(0, 1, false, qs0)]
        | depth (bnd,inc) ((k,np,rgd,q)::qs) =