# HG changeset patch
# User wenzelm
# Date 1308247979 -7200
# Node ID 7a7604573ecd2f5431e35d46d2b7ebbdb40f5649
# Parent  81517eed8a780768a8eb493b30635ba6f1837e61
explicit dependency on Pure.jar;

diff -r 81517eed8a78 -r 7a7604573ecd src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 16 18:00:56 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 16 20:12:59 2011 +0200
@@ -142,6 +142,11 @@
 
 ## dependencies
 
+[ -e "$ISABELLE_HOME/Admin/build" ] && \
+  { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
+
+PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
+
 pushd "$JEDIT_HOME" >/dev/null || failed
 
 JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"
@@ -176,9 +181,9 @@
     OUTDATED=true
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
-      declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}")
+      declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$PURE_JAR" "$JEDIT_JAR" "${JEDIT_JARS[@]}")
     else
-      declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}")
+      declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$PURE_JAR")
     fi
     for DEP in "${DEPS[@]}"
     do
@@ -196,11 +201,6 @@
 
 if [ "$OUTDATED" = true ]
 then
-  [ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable"
-
-  [ -e "$ISABELLE_HOME/Admin/build" ] && \
-    { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
-
   echo "###"
   echo "### Building Isabelle/jEdit ..."
   echo "###"
@@ -233,9 +233,7 @@
       print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
     print; }' dist/modes/catalog
 
-  cp -a "${JEDIT_JARS[@]}" "${SCALA_JARS[@]}" "$ISABELLE_HOME/lib/classes/Pure.jar" \
-    dist/jars/. || failed
-
+  cp -a "${JEDIT_JARS[@]}" "${SCALA_JARS[@]}" "$PURE_JAR" dist/jars/. || failed
   (
     for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar"
     do