more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
authorwenzelm
Mon, 16 Apr 2012 15:09:47 +0200
changeset 47490 f4348634595b
parent 47489 04e7d09ade7a
child 47491 62d93aec1846
child 47492 2631a12fb2d1
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
lib/scripts/getsettings
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick.ML
--- a/lib/scripts/getsettings	Mon Apr 16 11:24:57 2012 +0200
+++ b/lib/scripts/getsettings	Mon Apr 16 15:09:47 2012 +0200
@@ -97,7 +97,7 @@
 function isabelle_jdk () {
   if [ -z "$ISABELLE_JDK_HOME" ]; then
     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
-    return 2
+    return 127
   else
     local PRG="$1"; shift
     "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
@@ -108,10 +108,10 @@
 function isabelle_scala () {
   if [ -z "$ISABELLE_JDK_HOME" ]; then
     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
-    return 2
+    return 127
   elif [ -z "$SCALA_HOME" ]; then
     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
-    return 2
+    return 127
   else
     local PRG="$1"; shift
     "$SCALA_HOME/bin/$PRG" "$@"
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Apr 16 11:24:57 2012 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Apr 16 15:09:47 2012 +0200
@@ -1067,7 +1067,7 @@
                   TimedOut js
                 else if code = 0 then
                   Normal ([], js, first_error)
-                else if has_error "exec: java" then
+                else if code = 127 then
                   JavaNotInstalled
                 else if has_error "UnsupportedClassVersionError" then
                   JavaTooOld
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Apr 16 11:24:57 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Apr 16 15:09:47 2012 +0200
@@ -178,7 +178,7 @@
                (length ts downto 1) ts))]
 
 fun install_java_message () =
-  "Nitpick requires a Java 1.5 virtual machine called \"java\"."
+  "Nitpick requires Java Development Kit 1.6/1.7 via ISABELLE_JDK_HOME setting."
 fun install_kodkodi_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 \