--- a/src/HOL/Nitpick_Examples/minipick.ML Tue Sep 29 11:35:21 2020 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML Tue Sep 29 11:59:59 2020 +0200
@@ -436,8 +436,7 @@
in
case solve_any_problem debug overlord deadline max_threads max_solutions
problems of
- JavaNotFound => "unknown"
- | Normal ([], _, _) => "none"
+ Normal ([], _, _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"
| Error (s, _) => error ("Kodkod error: " ^ s)
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 29 11:35:21 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 29 11:59:59 2020 +0200
@@ -157,7 +157,6 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
- JavaNotFound |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -302,7 +301,6 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
- JavaNotFound |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -1063,8 +1061,6 @@
TimedOut js
else if rc = 0 then
Normal ([], js, first_error)
- else if rc = 127 then
- JavaNotFound
else if first_error <> "" then
Error (first_error, js)
else
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 29 11:35:21 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 29 11:59:59 2020 +0200
@@ -172,11 +172,6 @@
|> Syntax.pretty_term ctxt])
(length ts downto 1) ts))]
-val isabelle_wrong_message =
- "something appears to be wrong with your Isabelle installation"
-val java_not_found_message =
- "Java could not be launched -- " ^ isabelle_wrong_message
-
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
@@ -711,10 +706,7 @@
else
case KK.solve_any_problem debug overlord deadline max_threads
max_solutions (map fst problems) of
- KK.JavaNotFound =>
- (print_nt (K java_not_found_message);
- (found_really_genuine, max_potential, max_genuine, donno + 1))
- | KK.Normal ([], unsat_js, s) =>
+ KK.Normal ([], unsat_js, s) =>
(update_checked_problems problems unsat_js; show_kodkod_warning s;
(found_really_genuine, max_potential, max_genuine, donno))
| KK.Normal (sat_ps, unsat_js, s) =>