--- a/lib/Tools/console Tue Mar 08 17:55:11 2016 +0100
+++ b/lib/Tools/console Tue Mar 08 18:15:16 2016 +0100
@@ -4,7 +4,7 @@
#
# DESCRIPTION: run Isabelle process with raw ML console and line editor
-## settings
+isabelle_admin_build jars || exit $?
case "$ISABELLE_JAVA_PLATFORM" in
x86-*)
@@ -15,112 +15,8 @@
;;
esac
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS]"
- echo
- echo " Options are:"
- echo " -d DIR include session directory"
- echo " -l NAME logic session name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
- echo " -m MODE add print mode for output"
- echo " -n no build of session image on startup"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -r logic session is RAW_ML_SYSTEM"
- echo " -s system build mode for session image"
- echo
- echo " Run Isabelle process with raw ML console and line editor"
- echo " (ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")."
- echo
- exit 1
-}
-
-
-## process command line
-
-# options
-
-declare -a ISABELLE_OPTIONS=()
-
-declare -a INCLUDE_DIRS=()
-LOGIC="$ISABELLE_LOGIC"
-NO_BUILD="false"
-declare -a SYSTEM_OPTIONS=()
-SYSTEM_MODE="false"
-
-while getopts "d:l:m:no:rs" OPT
-do
- case "$OPT" in
- d)
- INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
- ;;
- l)
- LOGIC="$OPTARG"
- ;;
- m)
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
- ;;
- n)
- NO_BUILD="true"
- ;;
- o)
- SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
- ;;
- r)
- LOGIC="RAW_ML_SYSTEM"
- ;;
- s)
- SYSTEM_MODE="true"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## main
-
-isabelle_admin_build jars || exit $?
-
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
-if [ "$LOGIC" = "RAW_ML_SYSTEM" ]; then
- "$ISABELLE_TOOL" options -x "$OPTIONS_FILE"
-else
- "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Console \
- "$LOGIC" "$NO_BUILD" "$SYSTEM_MODE" "$OPTIONS_FILE" \
- "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
- rm -f "$OPTIONS_FILE"
- exit "$?"
- }
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="ASCII"
-fi
-
-ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
-ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
-
-if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
-then
- exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
-else
- echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
- exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
-fi
+"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"