doc-src/System/Thy/Basics.thy
changeset 45028 d608dd8cd409
parent 43564 9864182c6bad
child 47661 012a887997f3
equal deleted inserted replaced
45027:f459e93a038e 45028:d608dd8cd409
   330 
   330 
   331   Options are:
   331   Options are:
   332     -I           startup Isar interaction mode
   332     -I           startup Isar interaction mode
   333     -P           startup Proof General interaction mode
   333     -P           startup Proof General interaction mode
   334     -S           secure mode -- disallow critical operations
   334     -S           secure mode -- disallow critical operations
       
   335     -T ADDR      startup process wrapper, with socket address
   335     -W IN:OUT    startup process wrapper, with input/output fifos
   336     -W IN:OUT    startup process wrapper, with input/output fifos
   336     -X           startup PGIP interaction mode
   337     -X           startup PGIP interaction mode
   337     -e MLTEXT    pass MLTEXT to the ML session
   338     -e MLTEXT    pass MLTEXT to the ML session
   338     -f           pass 'Session.finish();' to the ML session
   339     -f           pass 'Session.finish();' to the ML session
   339     -m MODE      add print mode for output
   340     -m MODE      add print mode for output
   407   interaction mode on startup, instead of the primitive ML top-level.
   408   interaction mode on startup, instead of the primitive ML top-level.
   408   The @{verbatim "-P"} option configures the top-level loop for
   409   The @{verbatim "-P"} option configures the top-level loop for
   409   interaction with the Proof General user interface, and the
   410   interaction with the Proof General user interface, and the
   410   @{verbatim "-X"} option enables XML-based PGIP communication.
   411   @{verbatim "-X"} option enables XML-based PGIP communication.
   411 
   412 
   412   \medskip The @{verbatim "-W"} option makes Isabelle enter a special
   413   \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
   413   process wrapper for interaction via the Isabelle/Scala layer, see
   414   Isabelle enter a special process wrapper for interaction via the
   414   also @{file "~~/src/Pure/System/isabelle_process.scala"}.  The
   415   Isabelle/Scala layer, see also @{file
   415   protocol between the ML and JVM process is private to the
   416   "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
   416   implementation.
   417   the ML and JVM process is private to the implementation.
   417 
   418 
   418   \medskip The @{verbatim "-S"} option makes the Isabelle process more
   419   \medskip The @{verbatim "-S"} option makes the Isabelle process more
   419   secure by disabling some critical operations, notably runtime
   420   secure by disabling some critical operations, notably runtime
   420   compilation and evaluation of ML source code.
   421   compilation and evaluation of ML source code.
   421 *}
   422 *}