src/HOL/Tools/Nitpick/nitpick.ML
changeset 41772 27d4c768cf20
parent 41278 8e1cde88aae6
child 41789 7c7b68b06c1a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 18 15:44:52 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 18 16:19:08 2011 +0100
     1.3 @@ -981,15 +981,15 @@
     1.4    in (outcome_code, !state_ref) end
     1.5  
     1.6  (* Give the inner timeout a chance. *)
     1.7 -val timeout_bonus = seconds 0.25
     1.8 +val timeout_bonus = seconds 1.0
     1.9  
    1.10  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
    1.11                        step subst assm_ts orig_t =
    1.12 -  let val warning_m = if auto then K () else warning in
    1.13 +  let val print_m = if auto then K () else Output.urgent_message in
    1.14      if getenv "KODKODI" = "" then
    1.15        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    1.16           that the "Nitpick_Examples" can be processed on any machine. *)
    1.17 -      (warning_m (Pretty.string_of (plazy install_kodkodi_message));
    1.18 +      (print_m (Pretty.string_of (plazy install_kodkodi_message));
    1.19         ("no_kodkodi", state))
    1.20      else
    1.21        let
    1.22 @@ -1001,12 +1001,14 @@
    1.23                (pick_them_nits_in_term deadline state params auto i n step subst
    1.24                                        assm_ts) orig_t
    1.25            handle TOO_LARGE (_, details) =>
    1.26 -                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.27 +                 (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.28                 | TOO_SMALL (_, details) =>
    1.29 -                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.30 +                 (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.31                 | Kodkod.SYNTAX (_, details) =>
    1.32 -                 (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
    1.33 +                 (print_m ("Malformed Kodkodi output: " ^ details ^ ".");
    1.34                    unknown_outcome)
    1.35 +               | TimeLimit.TimeOut =>
    1.36 +                 (print_m "Nitpick ran out of time."; unknown_outcome)
    1.37        in
    1.38          if expect = "" orelse outcome_code = expect then outcome
    1.39          else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")