# HG changeset patch
# User wenzelm
# Date 1601373599 -7200
# Node ID 6255e532aa3662d56df6a130f9af0816111f8c09
# Parent  7cb0c5fbe2d9ee21a204728b4b96f043564742d6
obsolete --- Java is always present via component;

diff -r 7cb0c5fbe2d9 -r 6255e532aa36 src/HOL/Nitpick_Examples/minipick.ML
--- 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)
diff -r 7cb0c5fbe2d9 -r 6255e532aa36 src/HOL/Tools/Nitpick/kodkod.ML
--- 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
diff -r 7cb0c5fbe2d9 -r 6255e532aa36 src/HOL/Tools/Nitpick/nitpick.ML
--- 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) =>