# HG changeset patch
# User paulson
# Date 1061458904 -7200
# Node ID 6750ff1dfc32fd962f73c4177c2f1d95b1011857
# Parent  e2eba24c8a2abd4dda82b1e6a1d72e151ccbed43
Change from "tracing" to "warning", as requested by David Aspinall

diff -r e2eba24c8a2a -r 6750ff1dfc32 src/Pure/search.ML
--- a/src/Pure/search.ML	Wed Aug 20 13:34:17 2003 +0200
+++ b/src/Pure/search.ML	Thu Aug 21 11:41:44 2003 +0200
@@ -183,13 +183,15 @@
 (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   using increment "inc" up to limit "lim". *)
 fun DEEPEN (inc,lim) tacf m i = 
-  let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
-			    else if m>lim then 
-				(tracing "Giving up..."; no_tac)
-				 else (tracing ("Depth = " ^ string_of_int m);
-				       tacf m i  ORELSE  dpn (m+inc)))
+  let fun dpn m st = 
+       st |> (if has_fewer_prems i st then no_tac
+	      else if m>lim then 
+		       (warning "Search depth limit exceeded: giving up"; 
+			no_tac)
+	      else (warning ("Search depth = " ^ string_of_int m);
+			     tacf m i  ORELSE  dpn (m+inc)))
   in  dpn m  end;
-
+ 
 (*** Best-first search ***)
 
 val trace_BEST_FIRST = ref false;