# HG changeset patch
# User wenzelm
# Date 1414422684 -3600
# Node ID 00916b0dd596719dcc53df06a06baddcff00f13f
# Parent  a42a5129df91a2d31d5a06ce779b08de9971975c
clarified ISABELLE_JDK_HOME vs. JAVA_HOME;

diff -r a42a5129df91 -r 00916b0dd596 Admin/build
--- a/Admin/build	Mon Oct 27 16:00:04 2014 +0100
+++ b/Admin/build	Mon Oct 27 16:11:24 2014 +0100
@@ -24,8 +24,8 @@
   The MODULES list may contain any of the following:
 
     all             all modules below
-    browser         graph browser (requires jdk)
-    jars            Isabelle/Scala (requires \$ISABELLE_JDK_HOME and \$SCALA_HOME)
+    browser         graph browser
+    jars            Isabelle/Scala
     jars_test       test separate build of jars
     jars_fresh      fresh build of jars
 
diff -r a42a5129df91 -r 00916b0dd596 lib/Tools/java
--- a/lib/Tools/java	Mon Oct 27 16:00:04 2014 +0100
+++ b/lib/Tools/java	Mon Oct 27 16:11:24 2014 +0100
@@ -9,6 +9,6 @@
 [ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
 unset CLASSPATH
 
-isabelle_jdk java "${JAVA_ARGS[@]}" \
+isabelle_java java "${JAVA_ARGS[@]}" \
   -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
 
diff -r a42a5129df91 -r 00916b0dd596 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Oct 27 16:00:04 2014 +0100
+++ b/lib/scripts/getsettings	Mon Oct 27 16:11:24 2014 +0100
@@ -119,7 +119,7 @@
 function isabelle_jdk ()
 {
   if [ -z "$ISABELLE_JDK_HOME" ]; then
-    echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
+    echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
     return 127
   else
     local PRG="$1"; shift
@@ -127,11 +127,23 @@
   fi
 }
 
+#robust invocation via JAVA_HOME
+function isabelle_java ()
+{
+  if [ -z "$JAVA_HOME" ]; then
+    echo "Unknown JAVA_HOME -- Java unavailable" >&2
+    return 127
+  else
+    local PRG="$1"; shift
+    "$JAVA_HOME/bin/$PRG" "$@"
+  fi
+}
+
 #robust invocation via SCALA_HOME
 function isabelle_scala ()
 {
-  if [ -z "$ISABELLE_JDK_HOME" ]; then
-    echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
+  if [ -z "$JAVA_HOME" ]; then
+    echo "Unknown JAVA_HOME -- Java unavailable" >&2
     return 127
   elif [ -z "$SCALA_HOME" ]; then
     echo "Unknown SCALA_HOME -- Scala unavailable" >&2
@@ -261,7 +273,7 @@
 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
 
 #enforce JAVA_HOME
-export JAVA_HOME="$ISABELLE_JDK_HOME"
+export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
 
 #build condition etc.
 case "$ML_SYSTEM" in
diff -r a42a5129df91 -r 00916b0dd596 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Oct 27 16:00:04 2014 +0100
+++ b/src/Pure/build-jars	Mon Oct 27 16:11:24 2014 +0100
@@ -223,7 +223,7 @@
   SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"
 
   (
-    classpath "$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
+    classpath "$JAVA_HOME/lib/jfxrt.jar"
     classpath classes
     export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"