# HG changeset patch
# User blanchet
# Date 1266936973 -3600
# Node ID f61de25f71f9e677002fbec1c4ae9fde803c261b
# Parent  22442ab3e7a3504e658e9bd369aedef068f60209
distinguish between Kodkodi warnings and errors in Nitpick;
will be needed starting with version 1.2.9 of Kodkodi

diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Feb 23 15:56:13 2010 +0100
@@ -158,7 +158,7 @@
 
   datatype outcome =
     NotInstalled |
-    Normal of (int * raw_bound list) list * int list |
+    Normal of (int * raw_bound list) list * int list * string |
     TimedOut of int list |
     Interrupted of int list option |
     Error of string * int list
@@ -304,7 +304,7 @@
 
 datatype outcome =
   NotInstalled |
-  Normal of (int * raw_bound list) list * int list |
+  Normal of (int * raw_bound list) list * int list * string |
   TimedOut of int list |
   Interrupted of int list option |
   Error of string * int list
@@ -1029,7 +1029,7 @@
     val reindex = fst o nth indexed_problems
   in
     if null indexed_problems then
-      Normal ([], triv_js)
+      Normal ([], triv_js, "")
     else
       let
         val (serial_str, temp_dir) =
@@ -1089,6 +1089,8 @@
               if null ps then
                 if code = 2 then
                   TimedOut js
+                else if code = 0 then
+                  Normal ([], js, first_error)
                 else if first_error |> Substring.full
                         |> Substring.position "NoClassDefFoundError" |> snd
                         |> Substring.isEmpty |> not then
@@ -1098,12 +1100,10 @@
                                      |> perhaps (try (unprefix "Error: ")), js)
                 else if io_error then
                   Error ("I/O error", js)
-                else if code <> 0 then
+                else
                   Error ("Unknown error", js)
-                else
-                  Normal ([], js)
               else
-                Normal (ps, js)
+                Normal (ps, js, first_error)
             end
         in remove_temporary_files (); outcome end
         handle Exn.Interrupt =>
diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Tue Feb 23 15:56:13 2010 +0100
@@ -321,7 +321,7 @@
   in
     case solve_any_problem overlord NONE max_threads max_solutions problems of
       NotInstalled => "unknown"
-    | Normal ([], _) => "none"
+    | Normal ([], _, _) => "none"
     | Normal _ => "genuine"
     | TimedOut _ => "unknown"
     | Interrupted _ => "unknown"
diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 15:56:13 2010 +0100
@@ -412,7 +412,7 @@
       if sat_solver <> "smart" then
         if need_incremental andalso
            not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
-                      sat_solver) then
+                       sat_solver) then
           (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
                        \be used instead of " ^ quote sat_solver ^ "."));
            "SAT4J")
@@ -581,6 +581,9 @@
     fun update_checked_problems problems =
       List.app (Unsynchronized.change checked_problems o Option.map o cons
                 o nth problems)
+    (* string -> unit *)
+    fun show_kodkod_warning "" = ()
+      | show_kodkod_warning s = print_v (fn () => "Kodkod warning: " ^ s ^ ".")
 
     (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
     fun print_and_check_model genuine bounds
@@ -701,15 +704,16 @@
             KK.NotInstalled =>
             (print_m install_kodkodi_message;
              (max_potential, max_genuine, donno + 1))
-          | KK.Normal ([], unsat_js) =>
-            (update_checked_problems problems unsat_js;
+          | KK.Normal ([], unsat_js, s) =>
+            (update_checked_problems problems unsat_js; show_kodkod_warning s;
              (max_potential, max_genuine, donno))
-          | KK.Normal (sat_ps, unsat_js) =>
+          | KK.Normal (sat_ps, unsat_js, s) =>
             let
               val (lib_ps, con_ps) =
                 List.partition (#unsound o snd o nth problems o fst) sat_ps
             in
               update_checked_problems problems (unsat_js @ map fst lib_ps);
+              show_kodkod_warning s;
               if null con_ps then
                 let
                   val num_genuine = take max_potential lib_ps
diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Feb 23 15:56:13 2010 +0100
@@ -325,7 +325,7 @@
 fun run_all_tests () =
   case Kodkod.solve_any_problem false NONE 0 1
                                 (map (problem_for_nut @{context}) tests) of
-    Kodkod.Normal ([], _) => ()
+    Kodkod.Normal ([], _, _) => ()
   | _ => error "Tests failed"
 
 end;