diff -r c46418f12ee1 -r 83e815849a91 lib/Tools/console
--- 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 "$@"