# HG changeset patch
# User wenzelm
# Date 910606807 -3600
# Node ID a3881c1f1d3c5388673811037dc77b245cd12879
# Parent  4eea84a9427d3f91751372c19c388c1cc5313232
isabelle -I;

diff -r 4eea84a9427d -r a3881c1f1d3c doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Mon Nov 09 11:09:33 1998 +0100
+++ b/doc-src/System/basics.tex	Mon Nov 09 11:20:07 1998 +0100
@@ -221,6 +221,7 @@
 Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
 
   Options are:
+    -I           startup Isar interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
     -m MODE      add print mode for output
     -q           non-interactive session
@@ -274,9 +275,14 @@
 interface, for example to enable output of mathematical symbols from a
 special screen font.
 
-\medskip Isabelle normally enters an interactice {\ML} top-level loop
-(after processing the \texttt{-e} texts). The \texttt{-q} option
-inhibits this, thus providing a pure batch mode facility.
+\medskip Isabelle normally enters an interactice top-level loop (after
+processing the \texttt{-e} texts). The \texttt{-q} option inhibits this, thus
+providing a pure batch mode facility.
+
+\medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
+startup, instead of the primitive {\ML} top-level.  This flag is usually
+enabled by default when running Isabelle via some user interface, but it is
+\emph{not} for the basic \texttt{isabelle} program.
 
 
 \subsection*{Examples}
diff -r 4eea84a9427d -r a3881c1f1d3c doc-src/System/system.ind
--- a/doc-src/System/system.ind	Mon Nov 09 11:09:33 1998 +0100
+++ b/doc-src/System/system.ind	Mon Nov 09 11:20:07 1998 +0100
@@ -46,7 +46,7 @@
   \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 12, 17
   \item {\tt IsaMakefile}, 11, 12
   \item {\tt ISATOOL} setting, 3
-  \item {\tt isatool}, 1, 6
+  \item {\tt isatool}, 1, 7
 
   \indexspace