# HG changeset patch
# User blanchet
# Date 1298042348 -3600
# Node ID 27d4c768cf20c77ff6720fa3f3626e212d15645a
# Parent  70d4585b11a61ba6032f5879a5049e7f4e5d270a
make Nitpick's timeout mechanism somewhat more reliable/friendly;
avoid producing warnings when invoked in "auto" mode

diff -r 70d4585b11a6 -r 27d4c768cf20 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 18 15:44:52 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 18 16:19:08 2011 +0100
@@ -981,15 +981,15 @@
   in (outcome_code, !state_ref) end
 
 (* Give the inner timeout a chance. *)
-val timeout_bonus = seconds 0.25
+val timeout_bonus = seconds 1.0
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst assm_ts orig_t =
-  let val warning_m = if auto then K () else warning in
+  let val print_m = if auto then K () else Output.urgent_message in
     if getenv "KODKODI" = "" then
       (* The "expect" argument is deliberately ignored if Kodkodi is missing so
          that the "Nitpick_Examples" can be processed on any machine. *)
-      (warning_m (Pretty.string_of (plazy install_kodkodi_message));
+      (print_m (Pretty.string_of (plazy install_kodkodi_message));
        ("no_kodkodi", state))
     else
       let
@@ -1001,12 +1001,14 @@
               (pick_them_nits_in_term deadline state params auto i n step subst
                                       assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
-                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+                 (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
                | TOO_SMALL (_, details) =>
-                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+                 (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
                | Kodkod.SYNTAX (_, details) =>
-                 (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
+                 (print_m ("Malformed Kodkodi output: " ^ details ^ ".");
                   unknown_outcome)
+               | TimeLimit.TimeOut =>
+                 (print_m "Nitpick ran out of time."; unknown_outcome)
       in
         if expect = "" orelse outcome_code = expect then outcome
         else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")