# HG changeset patch
# User wenzelm
# Date 1197663335 -3600
# Node ID f7c6ca73a8bd9244c46a353ea6b85d0e318aa4de
# Parent  94bb4a85d35d940cd97622170e9002e7c25e2af8
added isatool tty;

diff -r 94bb4a85d35d -r f7c6ca73a8bd doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Fri Dec 14 21:15:34 2007 +0100
+++ b/doc-src/System/misc.tex	Fri Dec 14 21:15:35 2007 +0100
@@ -259,6 +259,27 @@
 printer spool command is determined by the \texttt{PRINT_COMMAND} setting.
 
 
+\section{Run Isabelle with plain tty interaction --- \texttt{isatool tty}} \label{sec:tool-tty}
+
+The \tooldx{tty} utility runs the Isabelle process interactively
+within a plain terminal session:
+\begin{ttbox}
+Usage: tty [OPTIONS]
+
+  Options are:
+    -l NAME      logic image name (default ISABELLE_LOGIC)
+    -m MODE      add print mode for output
+    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
+
+  Run Isabelle process with plain tty interaction, and optional line editor.
+\end{ttbox}
+
+The \texttt{-l} option specifies the logic image.  The \texttt{-m}
+option specifies additional print modes.  The The \texttt{-p} option
+specifies an alternative line editor (such as the \texttt{rlwrap}
+wrapper for GNU readline); the fall-back is to use raw standard input.
+
+
 \section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}}
 
 The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve
@@ -282,6 +303,7 @@
 Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007:
   November 2007}''.  There are no options nor arguments.
 
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "system"