uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;
--- a/etc/settings Fri Dec 05 11:42:27 2008 +0100
+++ b/etc/settings Fri Dec 05 18:15:52 2008 +0100
@@ -75,8 +75,11 @@
ISABELLE_SCALA="scala"
ISABELLE_JAVA="java"
-[ -e "$ISABELLE_HOME/contrib/scala" ] && \
+if [ -e "$ISABELLE_HOME/contrib/scala" ]; then
classpath "$ISABELLE_HOME/contrib/scala/lib/scala-library.jar"
+elif [ -e "$ISABELLE_HOME/../scala" ]; then
+ classpath "$ISABELLE_HOME/../scala/lib/scala-library.jar"
+fi
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
@@ -232,10 +235,22 @@
## Set HOME only for tools you have installed!
# External provers
-E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" \
- "$ISABELLE_HOME/contrib/SystemOnTPTP" "")
-SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
+E_HOME=$(choosefrom \
+ "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
+ "$ISABELLE_HOME/../E/$ML_PLATFORM" \
+ "/usr/local/E" \
+ "")
+VAMPIRE_HOME=$(choosefrom \
+ "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
+ "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
+ "/usr/local/Vampire" \
+ "$ISABELLE_HOME/contrib/SystemOnTPTP" \
+ "")
+SPASS_HOME=$(choosefrom \
+ "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
+ "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
+ "/usr/local/SPASS" \
+ "")
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"