# HG changeset patch # User wenzelm # Date 1334406996 -7200 # Node ID 71d5f37ee2bf68070aa8c9170b69588951603a3e # Parent b1cd02f2d534a856c35024c44e75079d0fcefbbb more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME; diff -r b1cd02f2d534 -r 71d5f37ee2bf lib/Tools/java --- a/lib/Tools/java Sat Apr 14 13:05:59 2012 +0200 +++ b/lib/Tools/java Sat Apr 14 14:36:36 2012 +0200 @@ -12,6 +12,6 @@ SERVER="" fi -exec "$ISABELLE_JDK_HOME/bin/java" -Dfile.encoding=UTF-8 $SERVER \ +isabelle_jdk java -Dfile.encoding=UTF-8 $SERVER \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r b1cd02f2d534 -r 71d5f37ee2bf lib/scripts/getsettings --- a/lib/scripts/getsettings Sat Apr 14 13:05:59 2012 +0200 +++ b/lib/scripts/getsettings Sat Apr 14 14:36:36 2012 +0200 @@ -95,18 +95,27 @@ #robust invocation via ISABELLE_JDK_HOME function isabelle_jdk () { - [ -z "$ISABELLE_JDK_HOME" ] && \ - { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2; return 2; } - local PRG="$1"; shift - "$ISABELLE_JDK_HOME/bin/$PRG" "$@" + if [ -z "$ISABELLE_JDK_HOME" ]; then + echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 + return 2 + else + local PRG="$1"; shift + "$ISABELLE_JDK_HOME/bin/$PRG" "$@" + fi } #robust invocation via SCALA_HOME function isabelle_scala () { - [ -z "$SCALA_HOME" ] && \ - { echo "Unknown SCALA_HOME -- Scala unavailable" >&2; return 2; } - local PRG="$1"; shift - "$SCALA_HOME/bin/$PRG" "$@" + if [ -z "$ISABELLE_JDK_HOME" ]; then + echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 + return 2 + elif [ -z "$SCALA_HOME" ]; then + echo "Unknown SCALA_HOME -- Scala unavailable" >&2 + return 2 + else + local PRG="$1"; shift + "$SCALA_HOME/bin/$PRG" "$@" + fi } #CLASSPATH convenience diff -r b1cd02f2d534 -r 71d5f37ee2bf src/Tools/JVM/java_ext_dirs --- a/src/Tools/JVM/java_ext_dirs Sat Apr 14 13:05:59 2012 +0200 +++ b/src/Tools/JVM/java_ext_dirs Sat Apr 14 14:36:36 2012 +0200 @@ -19,5 +19,5 @@ isabelle_jdk java \ -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \ - isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" + isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null