93 done |
93 done |
94 } |
94 } |
95 |
95 |
96 #robust invocation via ISABELLE_JDK_HOME |
96 #robust invocation via ISABELLE_JDK_HOME |
97 function isabelle_jdk () { |
97 function isabelle_jdk () { |
98 [ -z "$ISABELLE_JDK_HOME" ] && \ |
98 if [ -z "$ISABELLE_JDK_HOME" ]; then |
99 { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2; return 2; } |
99 echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
100 local PRG="$1"; shift |
100 return 2 |
101 "$ISABELLE_JDK_HOME/bin/$PRG" "$@" |
101 else |
|
102 local PRG="$1"; shift |
|
103 "$ISABELLE_JDK_HOME/bin/$PRG" "$@" |
|
104 fi |
102 } |
105 } |
103 |
106 |
104 #robust invocation via SCALA_HOME |
107 #robust invocation via SCALA_HOME |
105 function isabelle_scala () { |
108 function isabelle_scala () { |
106 [ -z "$SCALA_HOME" ] && \ |
109 if [ -z "$ISABELLE_JDK_HOME" ]; then |
107 { echo "Unknown SCALA_HOME -- Scala unavailable" >&2; return 2; } |
110 echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
108 local PRG="$1"; shift |
111 return 2 |
109 "$SCALA_HOME/bin/$PRG" "$@" |
112 elif [ -z "$SCALA_HOME" ]; then |
|
113 echo "Unknown SCALA_HOME -- Scala unavailable" >&2 |
|
114 return 2 |
|
115 else |
|
116 local PRG="$1"; shift |
|
117 "$SCALA_HOME/bin/$PRG" "$@" |
|
118 fi |
110 } |
119 } |
111 |
120 |
112 #CLASSPATH convenience |
121 #CLASSPATH convenience |
113 function classpath () { |
122 function classpath () { |
114 for X in "$@" |
123 for X in "$@" |