# HG changeset patch
# User blanchet
# Date 1346312866 -7200
# Node ID 224a0c63ba23dc4204d73575491960f2b90ded05
# Parent  5afe918dd476cffff5ad83fab53a538e583f2836
updated Java-related error message

diff -r 5afe918dd476 -r 224a0c63ba23 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -155,7 +155,7 @@
   type raw_bound = n_ary_index * int list list
 
   datatype outcome =
-    JavaNotInstalled |
+    JavaNotFound |
     JavaTooOld |
     KodkodiNotInstalled |
     Normal of (int * raw_bound list) list * int list * string |
@@ -302,7 +302,7 @@
 type raw_bound = n_ary_index * int list list
 
 datatype outcome =
-  JavaNotInstalled |
+  JavaNotFound |
   JavaTooOld |
   KodkodiNotInstalled |
   Normal of (int * raw_bound list) list * int list * string |
@@ -1068,7 +1068,7 @@
                 else if code = 0 then
                   Normal ([], js, first_error)
                 else if code = 127 then
-                  JavaNotInstalled
+                  JavaNotFound
                 else if has_error "UnsupportedClassVersionError" then
                   JavaTooOld
                 else if has_error "NoClassDefFoundError" then
diff -r 5afe918dd476 -r 224a0c63ba23 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -179,9 +179,13 @@
                                  Pretty.str (if j = 1 then "." else ";")])
                (length ts downto 1) ts))]
 
-fun install_java_message () =
-  "Nitpick requires Java Development Kit 1.6 via ISABELLE_JDK_HOME setting."
-fun install_kodkodi_message () =
+val isabelle_wrong_message =
+  "Something appears to be wrong with your Isabelle installation."
+fun java_not_found_message () =
+  "Java could not be launched. " ^ isabelle_wrong_message
+fun java_too_old_message () =
+  "The Java version is too old. " ^ isabelle_wrong_message
+fun kodkodi_not_installed_message () =
   "Nitpick requires the external Java program Kodkodi. To install it, download \
   \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \
   \\"kodkodi-x.y.z\" directory's full path to " ^
@@ -802,14 +806,14 @@
         else
           case KK.solve_any_problem debug overlord deadline max_threads
                                     max_solutions (map fst problems) of
-            KK.JavaNotInstalled =>
-            (print_nt install_java_message;
+            KK.JavaNotFound =>
+            (print_nt java_not_found_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
           | KK.JavaTooOld =>
-            (print_nt install_java_message;
+            (print_nt java_too_old_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
           | KK.KodkodiNotInstalled =>
-            (print_nt install_kodkodi_message;
+            (print_nt kodkodi_not_installed_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
           | KK.Normal ([], unsat_js, s) =>
             (update_checked_problems problems unsat_js; show_kodkod_warning s;
@@ -1062,7 +1066,7 @@
     if getenv "KODKODI" = "" then
       (* The "expect" argument is deliberately ignored if Kodkodi is missing so
          that the "Nitpick_Examples" can be processed on any machine. *)
-      (print_nt (Pretty.string_of (plazy install_kodkodi_message));
+      (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message));
        ("no_kodkodi", state))
     else
       let