doc-src/System/Thy/document/Basics.tex
changeset 45028 d608dd8cd409
parent 43564 9864182c6bad
child 47661 012a887997f3
--- a/doc-src/System/Thy/document/Basics.tex	Wed Sep 21 20:35:50 2011 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Wed Sep 21 22:18:17 2011 +0200
@@ -343,6 +343,7 @@
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
+    -T ADDR      startup process wrapper, with socket address
     -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
@@ -420,11 +421,10 @@
   interaction with the Proof General user interface, and the
   \verb|-X| option enables XML-based PGIP communication.
 
-  \medskip The \verb|-W| option makes Isabelle enter a special
-  process wrapper for interaction via the Isabelle/Scala layer, see
-  also \verb|~~/src/Pure/System/isabelle_process.scala|.  The
-  protocol between the ML and JVM process is private to the
-  implementation.
+  \medskip The \verb|-T| or \verb|-W| option makes
+  Isabelle enter a special process wrapper for interaction via the
+  Isabelle/Scala layer, see also \verb|~~/src/Pure/System/isabelle_process.scala|.  The protocol between
+  the ML and JVM process is private to the implementation.
 
   \medskip The \verb|-S| option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime