--- 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
--- 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