--- a/lib/Tools/build Thu Mar 10 17:30:04 2016 +0100
+++ b/lib/Tools/build Thu Mar 10 22:09:44 2016 +0100
@@ -4,7 +4,7 @@
#
# DESCRIPTION: build and manage Isabelle sessions
-## settings
+isabelle_admin_build jars || exit $?
case "$ISABELLE_JAVA_PLATFORM" in
x86-*)
@@ -15,174 +15,6 @@
;;
esac
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function show_settings()
-{
- local PREFIX="$1"
- echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
- echo
- echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_OPTIONS\""
- echo
- echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
- echo "${PREFIX}ML_HOME=\"$ML_HOME\""
- echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
- echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
-}
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
- echo
- echo " Options are:"
- echo " -D DIR include session directory and select its sessions"
- echo " -R operate on requirements of selected sessions"
- echo " -X NAME exclude sessions from group NAME and all descendants"
- echo " -a select all sessions"
- echo " -b build heap images"
- echo " -c clean build"
- echo " -d DIR include session directory"
- echo " -g NAME select session group NAME"
- echo " -j INT maximum number of parallel jobs (default 1)"
- echo " -k KEYWORD check theory sources for conflicts with proposed keywords"
- echo " -l list session source files"
- echo " -n no build -- test dependencies only"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -s system build mode: produce output in ISABELLE_HOME"
- echo " -v verbose"
- echo " -x NAME exclude session NAME and all descendants"
- echo
- echo " Build and manage Isabelle sessions, depending on implicit"
- show_settings " "
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function check_number()
-{
- [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
-}
-
-
-## process command line
-
-declare -a SELECT_DIRS=()
-REQUIREMENTS=false
-declare -a EXCLUDE_SESSION_GROUPS=()
-ALL_SESSIONS=false
-BUILD_HEAP=false
-CLEAN_BUILD=false
-declare -a INCLUDE_DIRS=()
-declare -a SESSION_GROUPS=()
-MAX_JOBS=1
-declare -a CHECK_KEYWORDS=()
-LIST_FILES=false
-NO_BUILD=false
-eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
-SYSTEM_MODE=false
-VERBOSE=false
-declare -a EXCLUDE_SESSIONS=()
+eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
-do
- case "$OPT" in
- D)
- SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
- ;;
- R)
- REQUIREMENTS="true"
- ;;
- X)
- EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
- ;;
- a)
- ALL_SESSIONS="true"
- ;;
- b)
- BUILD_HEAP="true"
- ;;
- c)
- CLEAN_BUILD="true"
- ;;
- d)
- INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
- ;;
- g)
- SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
- ;;
- j)
- check_number "$OPTARG"
- MAX_JOBS="$OPTARG"
- ;;
- k)
- CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
- ;;
- l)
- LIST_FILES="true"
- ;;
- n)
- NO_BUILD="true"
- ;;
- o)
- BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
- ;;
- s)
- SYSTEM_MODE="true"
- ;;
- v)
- VERBOSE="true"
- ;;
- x)
- EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-## main
-
-isabelle_admin_build jars || exit $?
-
-if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
- echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
-
- show_settings ""
- echo
-fi
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-. "$ISABELLE_HOME/lib/scripts/timestart.bash"
-
-isabelle java "${JAVA_ARGS[@]}" isabelle.Build \
- "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
- "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
- "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
- "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
- "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
- "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
-RC="$?"
-
-if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
- echo -n "Finished at "; date
-fi
-
-. "$ISABELLE_HOME/lib/scripts/timestop.bash"
-echo "$TIMES_REPORT"
-
-exit "$RC"
+exec isabelle java "${JAVA_ARGS[@]}" isabelle.Build "$@"