Change from "tracing" to "warning", as requested by David Aspinall
authorpaulson
Thu Aug 21 11:41:44 2003 +0200 (2003-08-21)
changeset 141606750ff1dfc32
parent 14159 e2eba24c8a2a
child 14161 73ad4884441f
Change from "tracing" to "warning", as requested by David Aspinall
src/Pure/search.ML
     1.1 --- a/src/Pure/search.ML	Wed Aug 20 13:34:17 2003 +0200
     1.2 +++ b/src/Pure/search.ML	Thu Aug 21 11:41:44 2003 +0200
     1.3 @@ -183,13 +183,15 @@
     1.4  (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
     1.5    using increment "inc" up to limit "lim". *)
     1.6  fun DEEPEN (inc,lim) tacf m i = 
     1.7 -  let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
     1.8 -			    else if m>lim then 
     1.9 -				(tracing "Giving up..."; no_tac)
    1.10 -				 else (tracing ("Depth = " ^ string_of_int m);
    1.11 -				       tacf m i  ORELSE  dpn (m+inc)))
    1.12 +  let fun dpn m st = 
    1.13 +       st |> (if has_fewer_prems i st then no_tac
    1.14 +	      else if m>lim then 
    1.15 +		       (warning "Search depth limit exceeded: giving up"; 
    1.16 +			no_tac)
    1.17 +	      else (warning ("Search depth = " ^ string_of_int m);
    1.18 +			     tacf m i  ORELSE  dpn (m+inc)))
    1.19    in  dpn m  end;
    1.20 -
    1.21 + 
    1.22  (*** Best-first search ***)
    1.23  
    1.24  val trace_BEST_FIRST = ref false;