1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 10:29:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 17:20:41 2010 +0200
     1.3 @@ -945,21 +945,32 @@
     1.4  
     1.5  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
     1.6                        step subst orig_assm_ts orig_t =
     1.7 -  if getenv "KODKODI" = "" then
     1.8 -    (if auto then ()
     1.9 -     else warning (Pretty.string_of (plazy install_kodkodi_message));
    1.10 -     ("unknown", state))
    1.11 -  else
    1.12 -    let
    1.13 -      val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    1.14 -      val outcome as (outcome_code, _) =
    1.15 -        time_limit (if debug then NONE else timeout)
    1.16 -            (pick_them_nits_in_term deadline state params auto i n step subst
    1.17 -                                    orig_assm_ts) orig_t
    1.18 -    in
    1.19 -      if expect = "" orelse outcome_code = expect then outcome
    1.20 -      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    1.21 -    end
    1.22 +  let
    1.23 +    val warning_m = if auto then K () else warning
    1.24 +    val unknown_outcome = ("unknown", state)
    1.25 +  in
    1.26 +    if getenv "KODKODI" = "" then
    1.27 +      (warning_m (Pretty.string_of (plazy install_kodkodi_message));
    1.28 +       unknown_outcome)
    1.29 +    else
    1.30 +      let
    1.31 +        val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    1.32 +        val outcome as (outcome_code, _) =
    1.33 +          time_limit (if debug then NONE else timeout)
    1.34 +              (pick_them_nits_in_term deadline state params auto i n step subst
    1.35 +                                      orig_assm_ts) orig_t
    1.36 +          handle TOO_LARGE (_, details) =>
    1.37 +                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.38 +               | TOO_SMALL (_, details) =>
    1.39 +                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
    1.40 +               | Kodkod.SYNTAX (_, details) =>
    1.41 +                 (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
    1.42 +                  unknown_outcome)
    1.43 +      in
    1.44 +        if expect = "" orelse outcome_code = expect then outcome
    1.45 +        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    1.46 +      end
    1.47 +  end
    1.48  
    1.49  fun is_fixed_equation fixes
    1.50                        (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =