--- a/Admin/CHECKLIST Mon Apr 09 20:42:05 2012 +0200
+++ b/Admin/CHECKLIST Mon Apr 09 20:57:23 2012 +0200
@@ -34,6 +34,9 @@
etc/components
lib/html/library_index_content.template
+- test separate compilation of Isabelle/Scala PIDE sources:
+ Admin/build jars_test
+
- test contrib components:
x86_64-linux without 32bit C/C++ libraries
Mac OS X Leopard
--- a/Admin/build Mon Apr 09 20:42:05 2012 +0200
+++ b/Admin/build Mon Apr 09 20:57:23 2012 +0200
@@ -28,6 +28,7 @@
doc documentation (requires latex and rail)
doc-src documentation sources from Isabelle theories
jars Isabelle/Scala layer (requires \$ISABELLE_JDK_HOME and \$SCALA_HOME)
+ jars_test test separate build of jars
jars_fresh fresh build of jars
EOF
@@ -121,6 +122,7 @@
doc-src) build_doc-src;;
jars) build_jars;;
jars_fresh) build_jars -f;;
+ jars_test) build_jars -t;;
*) fail "Bad module $MODULE"
esac
done
--- a/src/Pure/build-jars Mon Apr 09 20:42:05 2012 +0200
+++ b/src/Pure/build-jars Mon Apr 09 20:57:23 2012 +0200
@@ -77,6 +77,7 @@
echo
echo " Options are:"
echo " -f fresh build"
+ echo " -t test separate compilation of PIDE"
echo
exit 1
}
@@ -95,13 +96,17 @@
# options
FRESH=""
+TEST_PIDE=""
-while getopts "f" OPT
+while getopts "ft" OPT
do
case "$OPT" in
f)
FRESH=true
;;
+ t)
+ TEST_PIDE=true
+ ;;
\?)
usage
;;
@@ -171,11 +176,16 @@
SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"
- isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
- fail "Failed to compile PIDE sources"
-
- isabelle_scala scalac $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \
- fail "Failed to compile Pure sources"
+ if [ "$TEST_PIDE" = true ]; then
+ isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
+ fail "Failed to compile PIDE sources"
+ isabelle_scala scalac $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \
+ fail "Failed to compile Pure sources"
+ else
+ isabelle_scala scalac $SCALAC_OPTIONS -classpath classes \
+ "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
+ fail "Failed to compile sources"
+ fi
mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"