# HG changeset patch
# User wenzelm
# Date 1457039812 -3600
# Node ID 13d6948e4b12b1817baef6b0b39eb86c9c5d4f7d
# Parent  d0b68218ea5524e95bc5b7354ce12d0427b94013
isabelle console -r" helps to bootstrap Isabelle/Pure;

diff -r d0b68218ea55 -r 13d6948e4b12 NEWS
--- a/NEWS	Thu Mar 03 21:59:21 2016 +0100
+++ b/NEWS	Thu Mar 03 22:16:52 2016 +0100
@@ -1002,7 +1002,11 @@
 expressions (option -e) or files (option -f). Errors lead to premature
 exit of the ML process with return code 1.
 
-* Command-line tool "isabelle console" enables print mode "ASCII".
+* Command-line tool "isabelle console -r" helps to bootstrap
+Isabelle/Pure interactively.
+
+* Command-line tool "isabelle console" enables print mode "ASCII" for
+regular logic sessions.
 
 * Command-line tool "isabelle update_then" expands old Isar command
 conflations:
diff -r d0b68218ea55 -r 13d6948e4b12 lib/Tools/console
--- a/lib/Tools/console	Thu Mar 03 21:59:21 2016 +0100
+++ b/lib/Tools/console	Thu Mar 03 22:16:52 2016 +0100
@@ -31,6 +31,7 @@
   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"
@@ -52,7 +53,7 @@
 declare -a SYSTEM_OPTIONS=()
 SYSTEM_MODE="false"
 
-while getopts "d:l:m:no:s" OPT
+while getopts "d:l:m:no:rs" OPT
 do
   case "$OPT" in
     d)
@@ -71,6 +72,9 @@
     o)
       SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
       ;;
+    r)
+      LOGIC="RAW_ML_SYSTEM"
+      ;;
     s)
       SYSTEM_MODE="true"
       ;;
@@ -97,14 +101,15 @@
 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
 OPTIONS_FILE="$ISABELLE_TMP_PREFIX/options$$"
 
-"$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 "$?"
-}
-
-if [ "$LOGIC" != "RAW" ]; then
+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
diff -r d0b68218ea55 -r 13d6948e4b12 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Thu Mar 03 21:59:21 2016 +0100
+++ b/src/Doc/System/Misc.thy	Thu Mar 03 22:16:52 2016 +0100
@@ -65,10 +65,11 @@
 
   Options are:
     -d DIR       include session directory
-    -l NAME      logic session name (default ISABELLE_LOGIC)
+    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
     -m MODE      add print mode for output
     -n           no build of session image on startup
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -r           logic session is RAW_ML_SYSTEM
     -s           system build mode for session image
 
   Run Isabelle process with raw ML console and line editor
@@ -77,6 +78,9 @@
   The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default, its heap
   image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
 
+  Option \<^verbatim>\<open>-r\<close> abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
+  Isabelle/Pure interactively.
+
   Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
   (\secref{sec:tool-build}).