--- a/bin/isabelle_process Wed Mar 09 16:53:14 2016 +0100
+++ b/bin/isabelle_process Wed Mar 09 19:30:09 2016 +0100
@@ -9,248 +9,10 @@
exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
fi
-
-## settings
-
-PRG="$(basename "$0")"
-
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS] [HEAP]"
- echo
- echo " Options are:"
- echo " -O system options from given YXML file"
- echo " -P SOCKET startup process wrapper via TCP socket"
- echo " -S secure mode -- disallow critical operations"
- echo " -e ML_EXPR evaluate ML expression on startup"
- echo " -f ML_FILE evaluate ML file on startup"
- echo " -m MODE add print mode for output"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -q non-interactive session"
- echo
- echo " If HEAP is a plain name (default \"$ISABELLE_LOGIC\"), it is searched in \$ISABELLE_PATH;"
- echo " if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM,"
- echo " the initial ML heap is used."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-function check_file()
-{
- [ ! -f "$1" ] && fail "Bad file: \"$1\""
-}
-
-
-## process command line
-
-# options
-
-OPTIONS_FILE=""
-PROCESS_SOCKET=""
-SECURE=""
-declare -a LAST_ML_OPTIONS=()
-MODES=""
-declare -a SYSTEM_OPTIONS=()
-TERMINATE=""
-
-while getopts "O:P:Se:f:m:o:q" OPT
-do
- case "$OPT" in
- O)
- OPTIONS_FILE="$OPTARG"
- ;;
- P)
- PROCESS_SOCKET="$OPTARG"
- ;;
- S)
- SECURE=true
- ;;
- e)
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
- ;;
- f)
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--use"
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="$OPTARG"
- ;;
- m)
- if [ -z "$MODES" ]; then
- MODES="\"$OPTARG\""
- else
- MODES="\"$OPTARG\", $MODES"
- fi
- ;;
- o)
- SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
- ;;
- q)
- TERMINATE=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-HEAP=""
-
-if [ "$#" -ge 1 ]; then
- HEAP="$1"
- shift
-fi
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## check ML system
-
-[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
-
-
-## heap file
-
-declare -a FIRST_ML_OPTIONS=()
-
-[ -z "$HEAP" ] && HEAP="$ISABELLE_LOGIC"
+isabelle_admin_build jars || exit $?
-case "$HEAP" in
- RAW_ML_SYSTEM)
- HEAP_FILE=""
- ;;
- */*)
- HEAP_FILE="$HEAP"
- [ ! -f "$HEAP_FILE" ] && fail "Bad heap file: \"$HEAP_FILE\""
- ;;
- *)
- HEAP_FILE=""
- ISA_PATH=""
-
- splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
- for DIR in "${PATHS[@]}"
- do
- DIR="$DIR/$ML_IDENTIFIER"
- ISA_PATH="$ISA_PATH $DIR\n"
- [ -z "$HEAP_FILE" -a -f "$DIR/$HEAP" ] && HEAP_FILE="$DIR/$HEAP"
- done
-
- if [ -z "$HEAP_FILE" ]; then
- echo "Unknown logic \"$HEAP\" -- no heap file found in:" >&2
- echo -ne "$ISA_PATH" >&2
- exit 2
- fi
- ;;
-esac
-
-if [ -z "$HEAP_FILE" ]; then
- case "$ML_PLATFORM" in
- *-windows)
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
- ;;
- *)
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="fun exit rc = Posix.Process.exit (Word8.fromInt rc)"
- ;;
- esac
-else
- check_file "$HEAP_FILE"
- case "$ML_PLATFORM" in
- *-windows)
- PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
- ;;
- *)
- PLATFORM_HEAP_FILE="$HEAP_FILE"
- ;;
- esac
- PLATFORM_HEAP_FILE="$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$PLATFORM_HEAP_FILE")"
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.failure)"
-fi
-
-
-## prepare tmp directory
-
-[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
-ISABELLE_PID="$$"
-ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
-mkdir -p "$ISABELLE_TMP"
-chmod $(umask -S) "$ISABELLE_TMP"
-
-
-## ML text
-
-if [ -n "$MODES" ]; then
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Print_Mode.add_modes [$MODES]"
-fi
-
-if [ -n "$SECURE" ]; then
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Secure.set_secure ()"
-fi
-
-if [ -n "$PROCESS_SOCKET" ]; then
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="--eval"
- LAST_ML_OPTIONS["${#LAST_ML_OPTIONS[@]}"]="Isabelle_Process.init \"$PROCESS_SOCKET\""
-else
- ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
- if [ -n "$OPTIONS_FILE" ]; then
- [ "${#SYSTEM_OPTIONS[@]}" -gt 0 ] && \
- fail "Cannot provide options file and options on command-line"
- mv "$OPTIONS_FILE" "$ISABELLE_PROCESS_OPTIONS" ||
- fail "Failed to move options file \"$OPTIONS_FILE\""
- else
- "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
- fail "Failed to retrieve Isabelle system options"
- fi
- if [ "$HEAP" != RAW_ML_SYSTEM -a "$HEAP" != RAW ]; then
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Exn.capture_exit 2 Options.load_default ()"
- fi
-fi
-
-
-## ML process
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-export ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
-
-if [ -n "$TERMINATE" ]; then
- "$ML_HOME/poly" --error-exit -q -i $ML_OPTIONS \
- "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}" </dev/null
- RC="$?"
-else
- "$ISABELLE_HOME/lib/scripts/feeder" -p | \
- {
- read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS "${FIRST_ML_OPTIONS[@]}" "${LAST_ML_OPTIONS[@]}"
- RC="$?"
- kill -TERM "$FPID"
- exit "$RC"
- }
- RC="$?"
-fi
-
-[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
-rmdir "$ISABELLE_TMP"
-
-exit "$RC"
+"$ISABELLE_TOOL" java isabelle.Isabelle_Process "$@"