more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);

--- a/Admin/build	Mon Mar 26 15:38:09 2012 +0200
+++ b/Admin/build	Mon Mar 26 16:25:08 2012 +0200
@@ -27,7 +27,7 @@
     browser         graph browser (requires jdk)
     doc             documentation (requires latex and rail)
     doc-src         documentation sources from Isabelle theories
-    jars            Isabelle/Scala layer (requires Scala in \$SCALA_HOME)
+    jars            Isabelle/Scala layer (requires \$ISABELLE_JDK_HOME and \$SCALA_HOME)
     jars_fresh      fresh build of jars
 
 EOF

--- a/lib/Tools/java	Mon Mar 26 15:38:09 2012 +0200
+++ b/lib/Tools/java	Mon Mar 26 16:25:08 2012 +0200
@@ -6,21 +6,12 @@
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 
-JAVA_EXE="$ISABELLE_JDK_HOME/bin/java"
-
-if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
-  :
-else
-  echo "Bad Java executable: \"$JAVA_EXE\"" >&2
-  exit 2
-fi
-
-if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
+if isabelle_jdk java -server >/dev/null 2>/dev/null; then
   SERVER="-server"
 else
   SERVER=""
 fi
 
-exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
+exec "$ISABELLE_JDK_HOME/bin/java" -Dfile.encoding=UTF-8 $SERVER \
   "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
 

--- a/lib/Tools/scala	Mon Mar 26 15:38:09 2012 +0200
+++ b/lib/Tools/scala	Mon Mar 26 16:25:08 2012 +0200
@@ -4,10 +4,8 @@
 #
 # DESCRIPTION: invoke Scala within the Isabelle environment
 
-[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
-
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
+isabelle_scala scala -Dfile.encoding=UTF-8 \
   "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"

--- a/lib/Tools/scalac	Mon Mar 26 15:38:09 2012 +0200
+++ b/lib/Tools/scalac	Mon Mar 26 16:25:08 2012 +0200
@@ -4,10 +4,8 @@
 #
 # DESCRIPTION: invoke Scala compiler within the Isabelle environment
 
-[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
-
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \
+isabelle_scala scalac -Dfile.encoding=UTF-8 \
   "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"

--- a/lib/browser/build	Mon Mar 26 15:38:09 2012 +0200
+++ b/lib/browser/build	Mon Mar 26 16:25:08 2012 +0200
@@ -65,9 +65,9 @@
 
   rm -rf classes && mkdir classes
 
-  "$ISABELLE_JDK_HOME/bin/javac" -d classes -source 1.4 "${SOURCES[@]}" || \
+  isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \
     fail "Failed to compile sources"
-  "$ISABELLE_JDK_HOME/bin/jar" cf "$(jvmpath "$TARGET")" -C classes . ||
+  isabelle_jdk jar cf "$(jvmpath "$TARGET")" -C classes . ||
     fail "Failed to produce $TARGET"
 
   rm -rf classes

--- a/lib/scripts/getsettings	Mon Mar 26 15:38:09 2012 +0200
+++ b/lib/scripts/getsettings	Mon Mar 26 16:25:08 2012 +0200
@@ -89,6 +89,22 @@
   done
 }
 
+#robust invocation via ISABELLE_JDK_HOME
+function isabelle_jdk () {
+  [ -z "$ISABELLE_JDK_HOME" ] && \
+    { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; }
+  local PRG="$1"; shift
+  "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
+}
+
+#robust invocation via SCALA_HOME
+function isabelle_scala () {
+  [ -z "$SCALA_HOME" ] && \
+    { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
+  local PRG="$1"; shift
+  "$SCALA_HOME/bin/$PRG" "$@"
+}
+
 #CLASSPATH convenience
 function classpath () {
   for X in "$@"

--- a/src/Pure/build-jars	Mon Mar 26 15:38:09 2012 +0200
+++ b/src/Pure/build-jars	Mon Mar 26 16:25:08 2012 +0200
@@ -88,7 +88,6 @@
 }
 
 [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
-[ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable"
 
 
 ## process command line
@@ -172,10 +171,10 @@
 
   SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"
 
-  "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
+  isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
     fail "Failed to compile PIDE sources"
 
-  "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \
+  isabelle_scala scalac $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \
     fail "Failed to compile Pure sources"
 
   mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
@@ -186,7 +185,7 @@
   mkdir -p "$(dirname "$CHARSET_SERVICE")"
   echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"
 
-  "$ISABELLE_JDK_HOME/bin/jar" cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
+  isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
     fail "Failed to produce $TARGET"
 
   cp "$SCALA_HOME/lib/scala-swing.jar" "$SCALA_HOME/lib/scala-library.jar" "$TARGET_DIR/ext"

--- a/src/Tools/JVM/java_ext_dirs	Mon Mar 26 15:38:09 2012 +0200
+++ b/src/Tools/JVM/java_ext_dirs	Mon Mar 26 16:25:08 2012 +0200
@@ -17,7 +17,7 @@
 
 ## main
 
-exec "$ISABELLE_JDK_HOME/bin/java" \
+isabelle_jdk java \
   -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
   isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
 

--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Mar 26 15:38:09 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Mar 26 16:25:08 2012 +0200
@@ -248,7 +248,7 @@
   ) || fail "Failed to compile sources"
 
   cd dist/classes
-  "$ISABELLE_JDK_HOME/bin/jar" cf "../jars/Isabelle-jEdit.jar" * || failed
+  isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
   cd ../..
   rm -rf dist/classes
 fi