--- a/NEWS Mon Jun 30 09:31:32 2014 +0200
+++ b/NEWS Mon Jun 30 09:43:44 2014 +0200
@@ -894,6 +894,10 @@
incompatibility for old tools that do not use the $ISABELLE_PROCESS
settings variable yet.
+* Former "isabelle tty" has been superseded by "isabelle console",
+with implicit build like "isabelle jedit", and without the mostly
+obsolete Isar TTY loop.
+
* Removed obsolete "isabelle unsymbolize". Note that the usual format
for email communication is the Unicode rendering of Isabelle symbols,
as produced by Isabelle/jEdit, for example.
--- a/etc/settings Mon Jun 30 09:31:32 2014 +0200
+++ b/etc/settings Mon Jun 30 09:43:44 2014 +0200
@@ -26,9 +26,7 @@
### Interactive sessions (cf. isabelle tty)
###
-ISABELLE_LINE_EDITOR=""
-[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
-[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
+ISABELLE_LINE_EDITOR="rlwrap"
###
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/console Mon Jun 30 09:43:44 2014 +0200
@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: run Isabelle process with raw ML console and line editor
+
+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 " -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 BUILD_OPTIONS=()
+
+LOGIC="$ISABELLE_LOGIC"
+DO_BUILD="true"
+
+while getopts "d:l:m:no:s" OPT
+do
+ case "$OPT" in
+ d)
+ BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-d"
+ BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
+ ;;
+ l)
+ LOGIC="$OPTARG"
+ ;;
+ m)
+ ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
+ ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
+ ;;
+ n)
+ DO_BUILD="false"
+ ;;
+ o)
+ ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
+ ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
+ BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-o"
+ BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
+ ;;
+ s)
+ BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="-s"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
+
+
+## main
+
+if [ "$DO_BUILD" = true ]
+then
+ "$ISABELLE_TOOL" build -b -n "${BUILD_OPTIONS[@]}" "$LOGIC" >/dev/null 2>/dev/null ||
+ {
+ echo "Build started for Isabelle/$LOGIC"
+ "$ISABELLE_TOOL" build -b "${BUILD_OPTIONS[@]}" "$LOGIC" || exit "$?"
+ }
+fi
+
+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
--- a/lib/Tools/tty Mon Jun 30 09:31:32 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: run Isabelle process with plain tty interaction
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS]"
- echo
- echo " Options are:"
- echo " -l NAME logic image name (default ISABELLE_LOGIC=\"$ISABELLE_LOGIC\")"
- echo " -m MODE add print mode for output"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -p NAME line editor program name"
- echo " (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")"
- echo
- echo " Run Isabelle process with plain tty interaction and line editor."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-declare -a ISABELLE_OPTIONS=("-I")
-
-LOGIC=""
-LINE_EDITOR="$ISABELLE_LINE_EDITOR"
-
-while getopts "l:m:p:o:" OPT
-do
- case "$OPT" in
- l)
- LOGIC="$OPTARG"
- ;;
- m)
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
- ;;
- o)
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-o"
- ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTARG"
- ;;
- p)
- LINE_EDITOR="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## main
-
-if [ -n "$LINE_EDITOR" ]; then
- exec "$LINE_EDITOR" "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
-else
- exec "$ISABELLE_PROCESS" "${ISABELLE_OPTIONS[@]}" -- "$LOGIC"
-fi
--- a/src/Doc/System/Basics.thy Mon Jun 30 09:31:32 2014 +0200
+++ b/src/Doc/System/Basics.thy Mon Jun 30 09:43:44 2014 +0200
@@ -249,8 +249,8 @@
load if none is given explicitely by the user. The default value is
@{verbatim HOL}.
- \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
- line editor for the @{tool_ref tty} interface.
+ \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the
+ line editor for the @{tool_ref console} interface.
\item[@{setting_def ISABELLE_LATEX}, @{setting_def
ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}
@@ -350,7 +350,7 @@
*}
-section {* The raw Isabelle process *}
+section {* The raw Isabelle process \label{sec:isabelle-process} *}
text {*
The @{executable_def "isabelle_process"} executable runs bare-bones
--- a/src/Doc/System/Misc.thy Mon Jun 30 09:31:32 2014 +0200
+++ b/src/Doc/System/Misc.thy Mon Jun 30 09:43:44 2014 +0200
@@ -230,6 +230,47 @@
*}
+section {* Raw ML console *}
+
+text {*
+ The @{tool_def console} tool runs the Isabelle process with raw ML console:
+\begin{ttbox}
+Usage: isabelle console [OPTIONS]
+
+ Options are:
+ -d DIR include session directory
+ -l NAME logic session name (default ISABELLE_LOGIC)
+ -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)
+ -s system build mode for session image
+
+ Run Isabelle process with raw ML console and line editor
+ (default ISABELLE_LINE_EDITOR).
+\end{ttbox}
+
+ The @{verbatim "-l"} option specifies the logic session name. By default,
+ its heap image is checked and built on demand, but the option @{verbatim
+ "-n"} skips that.
+
+ Options @{verbatim "-d"}, @{verbatim "-o"}, @{verbatim "-s"} are passed
+ directly to @{tool build} (\secref{sec:tool-build}).
+
+ Options @{verbatim "-m"}, @{verbatim "-o"} are passed directly to the
+ underlying Isabelle process (\secref{sec:isabelle-process}).
+
+ The Isabelle process is run through the line editor that is specified via
+ the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
+ @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
+ standard input/output.
+
+ Interaction works via the raw ML toplevel loop: this is neither
+ Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful
+ ML commands at this stage are @{ML cd}, @{ML pwd}, @{ML use}, @{ML use_thy},
+ @{ML use_thys}.
+*}
+
+
section {* Displaying documents \label{sec:tool-display} *}
text {* The @{tool_def display} tool displays documents in DVI or PDF
@@ -420,39 +461,6 @@
using this template. *}
-section {* Plain TTY interaction \label{sec:tool-tty} *}
-
-text {*
- The @{tool_def tty} tool runs the Isabelle process interactively
- within a plain terminal session:
-\begin{ttbox}
-Usage: isabelle tty [OPTIONS]
-
- Options are:
- -l NAME logic image name (default ISABELLE_LOGIC)
- -m MODE add print mode for output
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -p NAME line editor program name (default ISABELLE_LINE_EDITOR)
-
- Run Isabelle process with plain tty interaction and line editor.
-\end{ttbox}
-
- The @{verbatim "-l"} option specifies the logic image. The
- @{verbatim "-m"} option specifies additional print modes. The
- @{verbatim "-p"} option specifies an alternative line editor (such
- as the @{executable_def rlwrap} wrapper for GNU readline); the
- fall-back is to use raw standard input.
-
- \medskip Option @{verbatim "-o"} allows to override Isabelle system
- options for this process, see also \secref{sec:system-options}.
-
- Regular interaction works via the standard Isabelle/Isar toplevel
- loop. The Isar command @{command exit} drops out into the
- bare-bones ML system, which is occasionally useful for debugging of
- the Isar infrastructure itself. Invoking @{ML Isar.loop}~@{verbatim
- "();"} in ML will return to the Isar toplevel. *}
-
-
section {* Output the version identifier of the Isabelle distribution *}
text {*