--- 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:
--- 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
--- 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}).