src/Doc/System/Basics.thy
changeset 52054 eaf17514aabd
parent 52052 892061142ba6
child 52056 fc458f304f93
     1.1 --- a/src/Doc/System/Basics.thy	Fri May 17 18:23:39 2013 +0200
     1.2 +++ b/src/Doc/System/Basics.thy	Fri May 17 18:39:49 2013 +0200
     1.3 @@ -378,11 +378,9 @@
     1.4      -T ADDR      startup process wrapper, with socket address
     1.5      -W IN:OUT    startup process wrapper, with input/output fifos
     1.6      -e MLTEXT    pass MLTEXT to the ML session
     1.7 -    -f           pass 'Session.finish();' to the ML session
     1.8      -m MODE      add print mode for output
     1.9      -q           non-interactive session
    1.10      -r           open heap file read-only
    1.11 -    -u           pass 'use"ROOT.ML";' to the ML session
    1.12      -w           reset write permissions on OUTPUT
    1.13  
    1.14    INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
    1.15 @@ -430,12 +428,6 @@
    1.16    may happen when errorneous ML code is provided. Also make sure that
    1.17    the ML commands are terminated properly by semicolon.
    1.18  
    1.19 -  \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
    1.20 -  "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
    1.21 -  The @{verbatim "-f"} option passes ``@{verbatim
    1.22 -  "Session.finish();"}'', which is intended mainly for administrative
    1.23 -  purposes.
    1.24 -
    1.25    \medskip The @{verbatim "-m"} option adds identifiers of print modes
    1.26    to be made active for this session. Typically, this is used by some
    1.27    user interface, e.g.\ to enable output of proper mathematical