# HG changeset patch
# User wenzelm
# Date 1404114224 -7200
# Node ID 0e41f26a025081dae0453d74d9651f4c54fc3d53
# Parent  663037c5d848602442f264a4bca53cf50b24fa9a
"isabelle tty" is superseded by "isabelle console";

diff -r 663037c5d848 -r 0e41f26a0250 NEWS
--- 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.
diff -r 663037c5d848 -r 0e41f26a0250 etc/settings
--- 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"
 
 
 ###
diff -r 663037c5d848 -r 0e41f26a0250 lib/Tools/console
--- /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
diff -r 663037c5d848 -r 0e41f26a0250 lib/Tools/tty
--- 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
diff -r 663037c5d848 -r 0e41f26a0250 src/Doc/System/Basics.thy
--- 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
diff -r 663037c5d848 -r 0e41f26a0250 src/Doc/System/Misc.thy
--- 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 {*