# HG changeset patch
# User blanchet
# Date 1268230000 -3600
# Node ID 17ae461d613342f654ee46aab62fd6c600813d99
# Parent  80b2c22f8f00c274949e89b78df8d6385bcc93a1
show nice error message in Nitpick when "java" is not available

diff -r 80b2c22f8f00 -r 17ae461d6133 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Mar 10 14:21:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Mar 10 15:06:40 2010 +0100
@@ -157,7 +157,8 @@
   type raw_bound = n_ary_index * int list list
 
   datatype outcome =
-    NotInstalled |
+    JavaNotInstalled |
+    KodkodiNotInstalled |
     Normal of (int * raw_bound list) list * int list * string |
     TimedOut of int list |
     Interrupted of int list option |
@@ -303,7 +304,8 @@
 type raw_bound = n_ary_index * int list list
 
 datatype outcome =
-  NotInstalled |
+  JavaNotInstalled |
+  KodkodiNotInstalled |
   Normal of (int * raw_bound list) list * int list * string |
   TimedOut of int list |
   Interrupted of int list option |
@@ -1095,9 +1097,13 @@
                 else if code = 0 then
                   Normal ([], js, first_error)
                 else if first_error |> Substring.full
+                        |> Substring.position "exec: java" |> snd
+                        |> Substring.isEmpty |> not then
+                  JavaNotInstalled
+                else if first_error |> Substring.full
                         |> Substring.position "NoClassDefFoundError" |> snd
                         |> Substring.isEmpty |> not then
-                  NotInstalled
+                  KodkodiNotInstalled
                 else if first_error <> "" then
                   Error (first_error, js)
                 else if io_error then
diff -r 80b2c22f8f00 -r 17ae461d6133 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 10 14:21:01 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 10 15:06:40 2010 +0100
@@ -149,6 +149,9 @@
                (length ts downto 1) ts))]
 
 (* unit -> string *)
+fun install_java_message () =
+  "Nitpick requires a Java 1.5 virtual machine called \"java\"."
+(* unit -> string *)
 fun install_kodkodi_message () =
   "Nitpick requires the external Java program Kodkodi. To install it, download \
   \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
@@ -726,7 +729,10 @@
         else
           case KK.solve_any_problem overlord deadline max_threads max_solutions
                                     (map fst problems) of
-            KK.NotInstalled =>
+            KK.JavaNotInstalled =>
+            (print_m install_java_message;
+             (found_really_genuine, max_potential, max_genuine, donno + 1))
+          | KK.KodkodiNotInstalled =>
             (print_m install_kodkodi_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
           | KK.Normal ([], unsat_js, s) =>
@@ -911,8 +917,7 @@
       in
         "Nitpick " ^ did_so_and_so ^
         (if is_some (!checked_problems) andalso total > 0 then
-           " after checking " ^
-           string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
+           " " ^ string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
            string_of_int total ^ " scope" ^ plural_s total
          else
            "") ^ "."
@@ -922,7 +927,7 @@
     fun run_batches _ _ []
                     (found_really_genuine, max_potential, max_genuine, donno) =
         if donno > 0 andalso max_genuine > 0 then
-          (print_m (fn () => excipit "ran out of some resource"); "unknown")
+          (print_m (fn () => excipit "checked"); "unknown")
         else if max_genuine = original_max_genuine then
           if max_potential = original_max_potential then
             (print_m (fn () =>
@@ -966,10 +971,11 @@
                    (false, max_potential, max_genuine, 0)
        handle Exn.Interrupt => do_interrupted ())
       handle TimeLimit.TimeOut =>
-             (print_m (fn () => excipit "ran out of time");
+             (print_m (fn () => excipit "ran out of time after checking");
               if !met_potential > 0 then "potential" else "unknown")
-           | Exn.Interrupt => if auto orelse debug then raise Interrupt
-                              else error (excipit "was interrupted")
+           | Exn.Interrupt =>
+             if auto orelse debug then raise Interrupt
+             else error (excipit "was interrupted after checking")
     val _ = print_v (fn () => "Total time: " ^
                               signed_string_of_int (Time.toMilliseconds
                                     (Timer.checkRealTimer timer)) ^ " ms.")