lib/scripts/getsettings
changeset 47115 1a05adae1cc9
parent 46741 a29006291f2b
child 47254 de2fb19683f4
--- 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 "$@"