doc-src/System/Thy/document/Basics.tex
changeset 45028 d608dd8cd409
parent 43564 9864182c6bad
child 47661 012a887997f3
equal deleted inserted replaced
45027:f459e93a038e 45028:d608dd8cd409
   341 
   341 
   342   Options are:
   342   Options are:
   343     -I           startup Isar interaction mode
   343     -I           startup Isar interaction mode
   344     -P           startup Proof General interaction mode
   344     -P           startup Proof General interaction mode
   345     -S           secure mode -- disallow critical operations
   345     -S           secure mode -- disallow critical operations
       
   346     -T ADDR      startup process wrapper, with socket address
   346     -W IN:OUT    startup process wrapper, with input/output fifos
   347     -W IN:OUT    startup process wrapper, with input/output fifos
   347     -X           startup PGIP interaction mode
   348     -X           startup PGIP interaction mode
   348     -e MLTEXT    pass MLTEXT to the ML session
   349     -e MLTEXT    pass MLTEXT to the ML session
   349     -f           pass 'Session.finish();' to the ML session
   350     -f           pass 'Session.finish();' to the ML session
   350     -m MODE      add print mode for output
   351     -m MODE      add print mode for output
   418   interaction mode on startup, instead of the primitive ML top-level.
   419   interaction mode on startup, instead of the primitive ML top-level.
   419   The \verb|-P| option configures the top-level loop for
   420   The \verb|-P| option configures the top-level loop for
   420   interaction with the Proof General user interface, and the
   421   interaction with the Proof General user interface, and the
   421   \verb|-X| option enables XML-based PGIP communication.
   422   \verb|-X| option enables XML-based PGIP communication.
   422 
   423 
   423   \medskip The \verb|-W| option makes Isabelle enter a special
   424   \medskip The \verb|-T| or \verb|-W| option makes
   424   process wrapper for interaction via the Isabelle/Scala layer, see
   425   Isabelle enter a special process wrapper for interaction via the
   425   also \verb|~~/src/Pure/System/isabelle_process.scala|.  The
   426   Isabelle/Scala layer, see also \verb|~~/src/Pure/System/isabelle_process.scala|.  The protocol between
   426   protocol between the ML and JVM process is private to the
   427   the ML and JVM process is private to the implementation.
   427   implementation.
       
   428 
   428 
   429   \medskip The \verb|-S| option makes the Isabelle process more
   429   \medskip The \verb|-S| option makes the Isabelle process more
   430   secure by disabling some critical operations, notably runtime
   430   secure by disabling some critical operations, notably runtime
   431   compilation and evaluation of ML source code.%
   431   compilation and evaluation of ML source code.%
   432 \end{isamarkuptext}%
   432 \end{isamarkuptext}%