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 if [ -z "$ISABELLE_JDK_HOME" ]; then |
98 if [ -z "$ISABELLE_JDK_HOME" ]; then |
99 echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
99 echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
100 return 2 |
100 return 127 |
101 else |
101 else |
102 local PRG="$1"; shift |
102 local PRG="$1"; shift |
103 "$ISABELLE_JDK_HOME/bin/$PRG" "$@" |
103 "$ISABELLE_JDK_HOME/bin/$PRG" "$@" |
104 fi |
104 fi |
105 } |
105 } |
106 |
106 |
107 #robust invocation via SCALA_HOME |
107 #robust invocation via SCALA_HOME |
108 function isabelle_scala () { |
108 function isabelle_scala () { |
109 if [ -z "$ISABELLE_JDK_HOME" ]; then |
109 if [ -z "$ISABELLE_JDK_HOME" ]; then |
110 echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
110 echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2 |
111 return 2 |
111 return 127 |
112 elif [ -z "$SCALA_HOME" ]; then |
112 elif [ -z "$SCALA_HOME" ]; then |
113 echo "Unknown SCALA_HOME -- Scala unavailable" >&2 |
113 echo "Unknown SCALA_HOME -- Scala unavailable" >&2 |
114 return 2 |
114 return 127 |
115 else |
115 else |
116 local PRG="$1"; shift |
116 local PRG="$1"; shift |
117 "$SCALA_HOME/bin/$PRG" "$@" |
117 "$SCALA_HOME/bin/$PRG" "$@" |
118 fi |
118 fi |
119 } |
119 } |