# HG changeset patch
# User blanchet
# Date 1282120924 -7200
# Node ID 307669429dc155d1eed9cbed2730da13e67c0f90
# Parent  32391240695f84532db64a98c89c74a4f6465e8d
gracefully handle the case where the JVM is too old in Nitpick

diff -r 32391240695f -r 307669429dc1 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Wed Aug 18 09:38:50 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Wed Aug 18 10:42:04 2010 +0200
@@ -116,7 +116,7 @@
 C-n. This is equivalent to entering the \textbf{nitpick} command with no
 arguments in the theory text.
 
-Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
+Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.6 virtual
 machine called \texttt{java}. The examples presented in this manual can be found
 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
 
diff -r 32391240695f -r 307669429dc1 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Aug 18 09:38:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Aug 18 10:42:04 2010 +0200
@@ -156,6 +156,7 @@
 
   datatype outcome =
     JavaNotInstalled |
+    JavaTooOld |
     KodkodiNotInstalled |
     Normal of (int * raw_bound list) list * int list * string |
     TimedOut of int list |
@@ -303,6 +304,7 @@
 
 datatype outcome =
   JavaNotInstalled |
+  JavaTooOld |
   KodkodiNotInstalled |
   Normal of (int * raw_bound list) list * int list * string |
   TimedOut of int list |
@@ -1063,19 +1065,20 @@
                 |> perhaps (try (unsuffix "."))
                 |> perhaps (try (unprefix "Solve error: "))
                 |> perhaps (try (unprefix "Error: "))
+              fun has_error s =
+                first_error |> Substring.full |> Substring.position s |> snd
+                            |> Substring.isEmpty |> not
             in
               if null ps then
                 if code = 2 then
                   TimedOut js
                 else if code = 0 then
                   Normal ([], js, first_error)
-                else if first_error |> Substring.full
-                        |> Substring.position "exec: java" |> snd
-                        |> Substring.isEmpty |> not then
+                else if has_error "exec: java" then
                   JavaNotInstalled
-                else if first_error |> Substring.full
-                        |> Substring.position "NoClassDefFoundError" |> snd
-                        |> Substring.isEmpty |> not then
+                else if has_error "UnsupportedClassVersionError" then
+                  JavaTooOld
+                else if has_error "NoClassDefFoundError" then
                   KodkodiNotInstalled
                 else if first_error <> "" then
                   Error (first_error, js)
diff -r 32391240695f -r 307669429dc1 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Aug 18 09:38:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Aug 18 10:42:04 2010 +0200
@@ -315,6 +315,7 @@
   in
     case solve_any_problem overlord NONE max_threads max_solutions problems of
       JavaNotInstalled => "unknown"
+    | JavaTooOld => "unknown"
     | KodkodiNotInstalled => "unknown"
     | Normal ([], _, _) => "none"
     | Normal _ => "genuine"
diff -r 32391240695f -r 307669429dc1 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Aug 18 09:38:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Aug 18 10:42:04 2010 +0200
@@ -158,7 +158,7 @@
                (length ts downto 1) ts))]
 
 fun install_java_message () =
-  "Nitpick requires a Java 1.5 virtual machine called \"java\"."
+  "Nitpick requires a Java 1.6 virtual machine called \"java\"."
 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\" \
@@ -740,6 +740,9 @@
             KK.JavaNotInstalled =>
             (print_m install_java_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
+          | KK.JavaTooOld =>
+            (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))