src/Doc/System/Basics.thy
changeset 51932 f196352201d6
parent 51434 e19a22974c72
child 52052 892061142ba6
     1.1 --- a/src/Doc/System/Basics.thy	Sat May 11 18:16:17 2013 +0200
     1.2 +++ b/src/Doc/System/Basics.thy	Sat May 11 18:45:38 2013 +0200
     1.3 @@ -383,7 +383,6 @@
     1.4      -S           secure mode -- disallow critical operations
     1.5      -T ADDR      startup process wrapper, with socket address
     1.6      -W IN:OUT    startup process wrapper, with input/output fifos
     1.7 -    -X           startup PGIP interaction mode
     1.8      -e MLTEXT    pass MLTEXT to the ML session
     1.9      -f           pass 'Session.finish();' to the ML session
    1.10      -m MODE      add print mode for output
    1.11 @@ -456,8 +455,7 @@
    1.12    \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
    1.13    interaction mode on startup, instead of the primitive ML top-level.
    1.14    The @{verbatim "-P"} option configures the top-level loop for
    1.15 -  interaction with the Proof General user interface, and the
    1.16 -  @{verbatim "-X"} option enables XML-based PGIP communication.
    1.17 +  interaction with the Proof General user interface.
    1.18  
    1.19    \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
    1.20    Isabelle enter a special process wrapper for interaction via