# HG changeset patch
# User wenzelm
# Date 1160417565 -7200
# Node ID 7ab9fa7d658fd676cd3da92ed8fa69afd3f020b0
# Parent  cd2a6d00ec47085e8fec7a65bda48d28600baf97
isabelle-process: options -S, -X;

diff -r cd2a6d00ec47 -r 7ab9fa7d658f doc-src/System/basics.tex
--- a/doc-src/System/basics.tex	Mon Oct 09 20:12:42 2006 +0200
+++ b/doc-src/System/basics.tex	Mon Oct 09 20:12:45 2006 +0200
@@ -269,6 +269,8 @@
     -C           tell ML system to copy output image
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
+    -S           secure mode -- disallow critical operations
+    -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
@@ -304,7 +306,7 @@
 
 The read-write state of sessions is determined at startup only, it cannot be
 changed intermediately. Also note that heap images may require considerable
-amounts of disk space (approximately 20--40~MB). Users are responsible for
+amounts of disk space (approximately 40--80~MB). Users are responsible for
 themselves to dispose their heap files when they are no longer needed.
 
 \medskip The \texttt{-w} option makes the output heap file read-only after
@@ -339,10 +341,15 @@
 processing the \texttt{-e} texts). The \texttt{-q} option inhibits
 interaction, 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.  The \texttt{-P} option
-configures the top-level loop for interaction with the Proof~General user
-interface; do not enable this in plain TTY sessions.
+\medskip The \texttt{-I} option makes Isabelle enter Isar interaction
+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.
+
+\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.
 
 
 \subsection*{Examples}