doc-src/System/Thy/Basics.thy
changeset 45028 d608dd8cd409
parent 43564 9864182c6bad
child 47661 012a887997f3
     1.1 --- a/doc-src/System/Thy/Basics.thy	Wed Sep 21 20:35:50 2011 +0200
     1.2 +++ b/doc-src/System/Thy/Basics.thy	Wed Sep 21 22:18:17 2011 +0200
     1.3 @@ -332,6 +332,7 @@
     1.4      -I           startup Isar interaction mode
     1.5      -P           startup Proof General interaction mode
     1.6      -S           secure mode -- disallow critical operations
     1.7 +    -T ADDR      startup process wrapper, with socket address
     1.8      -W IN:OUT    startup process wrapper, with input/output fifos
     1.9      -X           startup PGIP interaction mode
    1.10      -e MLTEXT    pass MLTEXT to the ML session
    1.11 @@ -409,11 +410,11 @@
    1.12    interaction with the Proof General user interface, and the
    1.13    @{verbatim "-X"} option enables XML-based PGIP communication.
    1.14  
    1.15 -  \medskip The @{verbatim "-W"} option makes Isabelle enter a special
    1.16 -  process wrapper for interaction via the Isabelle/Scala layer, see
    1.17 -  also @{file "~~/src/Pure/System/isabelle_process.scala"}.  The
    1.18 -  protocol between the ML and JVM process is private to the
    1.19 -  implementation.
    1.20 +  \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
    1.21 +  Isabelle enter a special process wrapper for interaction via the
    1.22 +  Isabelle/Scala layer, see also @{file
    1.23 +  "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
    1.24 +  the ML and JVM process is private to the implementation.
    1.25  
    1.26    \medskip The @{verbatim "-S"} option makes the Isabelle process more
    1.27    secure by disabling some critical operations, notably runtime