# HG changeset patch
# User wenzelm
# Date 1196804962 -3600
# Node ID 79f198a08c15c2f130ff8e4322b2d90b5e0ea0a2
# Parent  08b0feb07239287808fcf8904d0c388e0e2e8c5a
isabelle process: replaced option -p by -W (process wrapper);

diff -r 08b0feb07239 -r 79f198a08c15 doc-src/System/basics.tex
--- 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}