equal
deleted
inserted
replaced
87 ;; |
87 ;; |
88 esac |
88 esac |
89 done |
89 done |
90 } |
90 } |
91 |
91 |
|
92 #robust invocation via ISABELLE_JDK_HOME |
|
93 function isabelle_jdk () { |
|
94 [ -z "$ISABELLE_JDK_HOME" ] && \ |
|
95 { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; } |
|
96 local PRG="$1"; shift |
|
97 "$ISABELLE_JDK_HOME/bin/$PRG" "$@" |
|
98 } |
|
99 |
|
100 #robust invocation via SCALA_HOME |
|
101 function isabelle_scala () { |
|
102 [ -z "$SCALA_HOME" ] && \ |
|
103 { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; } |
|
104 local PRG="$1"; shift |
|
105 "$SCALA_HOME/bin/$PRG" "$@" |
|
106 } |
|
107 |
92 #CLASSPATH convenience |
108 #CLASSPATH convenience |
93 function classpath () { |
109 function classpath () { |
94 for X in "$@" |
110 for X in "$@" |
95 do |
111 do |
96 if [ -z "$CLASSPATH" ]; then |
112 if [ -z "$CLASSPATH" ]; then |