DEEPEN: Use priority message channel for interim messages (not warnings).
authoraspinall
Wed Jul 18 14:46:59 2007 +0200 (2007-07-18)
changeset 23841598839baafed
parent 23840 0295493ba748
child 23842 9d87177f1f89
DEEPEN: Use priority message channel for interim messages (not warnings).
src/Pure/search.ML
     1.1 --- a/src/Pure/search.ML	Wed Jul 18 14:44:49 2007 +0200
     1.2 +++ b/src/Pure/search.ML	Wed Jul 18 14:46:59 2007 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4                else if m>lim then
     1.5                         (warning "Search depth limit exceeded: giving up";
     1.6                          no_tac)
     1.7 -              else (warning ("Search depth = " ^ string_of_int m);
     1.8 +              else (priority ("Search depth = " ^ string_of_int m);
     1.9                               tacf m i  ORELSE  dpn (m+inc)))
    1.10    in  dpn m  end;
    1.11