1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 14:50:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 15:56:13 2010 +0100
     1.3 @@ -412,7 +412,7 @@
     1.4        if sat_solver <> "smart" then
     1.5          if need_incremental andalso
     1.6             not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
     1.7 -                      sat_solver) then
     1.8 +                       sat_solver) then
     1.9            (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
    1.10                         \be used instead of " ^ quote sat_solver ^ "."));
    1.11             "SAT4J")
    1.12 @@ -581,6 +581,9 @@
    1.13      fun update_checked_problems problems =
    1.14        List.app (Unsynchronized.change checked_problems o Option.map o cons
    1.15                  o nth problems)
    1.16 +    (* string -> unit *)
    1.17 +    fun show_kodkod_warning "" = ()
    1.18 +      | show_kodkod_warning s = print_v (fn () => "Kodkod warning: " ^ s ^ ".")
    1.19  
    1.20      (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
    1.21      fun print_and_check_model genuine bounds
    1.22 @@ -701,15 +704,16 @@
    1.23              KK.NotInstalled =>
    1.24              (print_m install_kodkodi_message;
    1.25               (max_potential, max_genuine, donno + 1))
    1.26 -          | KK.Normal ([], unsat_js) =>
    1.27 -            (update_checked_problems problems unsat_js;
    1.28 +          | KK.Normal ([], unsat_js, s) =>
    1.29 +            (update_checked_problems problems unsat_js; show_kodkod_warning s;
    1.30               (max_potential, max_genuine, donno))
    1.31 -          | KK.Normal (sat_ps, unsat_js) =>
    1.32 +          | KK.Normal (sat_ps, unsat_js, s) =>
    1.33              let
    1.34                val (lib_ps, con_ps) =
    1.35                  List.partition (#unsound o snd o nth problems o fst) sat_ps
    1.36              in
    1.37                update_checked_problems problems (unsat_js @ map fst lib_ps);
    1.38 +              show_kodkod_warning s;
    1.39                if null con_ps then
    1.40                  let
    1.41                    val num_genuine = take max_potential lib_ps