doc-src/System/Thy/document/Basics.tex

     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
     -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
     -X           startup PGIP interaction mode
-    -c           tell ML system to compress output image
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
     -m MODE      add print mode for output
     -q           non-interactive session
     -r           open heap file read-only

 
   \medskip The \verb|-w| option makes the output heap file
   read-only after terminating.  Thus subsequent invocations cause the
   logic image to be read-only automatically.
 
-  \medskip The \verb|-c| option tells the underlying ML system
-  to compress the output heap (fully transparently).  On Poly/ML for
-  example, the image is garbage collected and all stored values are
-  maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
-  consumption.
-
   \medskip Using the \verb|-e| option, arbitrary ML code may be
   passed to the Isabelle session from the command line. Multiple
   \verb|-e|'s are evaluated in the given order. Strange things
   may happen when errorneous ML code is provided. Also make sure that
   the ML commands are terminated properly by semicolon.