# HG changeset patch
# User aspinall
# Date 1184762819 -7200
# Node ID 598839baafeda437e067889322a49a1563bece1f
# Parent  0295493ba748403ccd9389108eb6fc366deb39f5
DEEPEN: Use priority message channel for interim messages (not warnings).

diff -r 0295493ba748 -r 598839baafed src/Pure/search.ML
--- a/src/Pure/search.ML	Wed Jul 18 14:44:49 2007 +0200
+++ b/src/Pure/search.ML	Wed Jul 18 14:46:59 2007 +0200
@@ -196,7 +196,7 @@
               else if m>lim then
                        (warning "Search depth limit exceeded: giving up";
                         no_tac)
-              else (warning ("Search depth = " ^ string_of_int m);
+              else (priority ("Search depth = " ^ string_of_int m);
                              tacf m i  ORELSE  dpn (m+inc)))
   in  dpn m  end;