--- a/doc-src/System/basics.tex Tue Dec 04 22:49:21 2007 +0100
+++ b/doc-src/System/basics.tex Tue Dec 04 22:49:22 2007 +0100
@@ -281,12 +281,12 @@
-I startup Isar interaction mode
-P startup Proof General interaction mode
-S secure mode -- disallow critical operations
+ -W startup process wrapper (interaction via external program)
-X startup PGIP interaction mode
-c tell ML system to compress output image
-e MLTEXT pass MLTEXT to the ML session
-f pass 'Session.finish();' to the ML session
-m MODE add print mode for output
- -p echo ISABELLE_PID on startup
-q non-interactive session
-r open heap file read-only
-u pass 'use"ROOT.ML";' to the ML session
@@ -357,18 +357,15 @@
mode on startup, instead of the primitive {\ML} top-level. The
\texttt{-P} option configures the top-level loop for interaction with
the Proof~General user interface, and the \texttt{-X} option enables
-XML-based PGIP communication.
+XML-based PGIP communication. The \texttt{-W} option makes Isabelle
+enter a special process wrapper for interaction via an external
+program; the protocol is a stripped-down version of Proof~General the
+interaction mode.
\medskip The \texttt{-S} option makes the Isabelle process more secure
by disabling some critical operations, notably runtime compilation and
evaluation of ML source code.
-\medskip The \texttt{-p} option echos the \texttt{ISABELLE_PID}
-variable on startup, which is the operating system identifier of the
-Isabelle process group. This enables to control the process later on,
-e.g.\ sending an interrupt signal like this: \verb,kill -INT -,$pid$
-(the $pid$ is negated here to address the whole process group).
-
\subsection*{Examples}