discontinued obsolete isabelle-process options -f and -u;
authorwenzelm
Fri May 17 18:39:49 2013 +0200 (2013-05-17)
changeset 52054eaf17514aabd
parent 52053 5ffb9bad6517
child 52055 10bc73197a57
discontinued obsolete isabelle-process options -f and -u;
NEWS
bin/isabelle-process
src/Doc/System/Basics.thy
src/Pure/build
     1.1 --- a/NEWS	Fri May 17 18:23:39 2013 +0200
     1.2 +++ b/NEWS	Fri May 17 18:39:49 2013 +0200
     1.3 @@ -235,6 +235,9 @@
     1.4  * Discontinued obsolete isabelle usedir, mkdir, make -- superseded by
     1.5  "isabelle build" in Isabelle2013.  INCOMPATIBILITY.
     1.6  
     1.7 +* Discontinued obsolete isabelle-process options -f and -u (former
     1.8 +administrative aliases of option -e).  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
    1.11  specify global resources of the JVM process run by isabelle build.
    1.12  
     2.1 --- a/bin/isabelle-process	Fri May 17 18:23:39 2013 +0200
     2.2 +++ b/bin/isabelle-process	Fri May 17 18:39:49 2013 +0200
     2.3 @@ -32,11 +32,9 @@
     2.4    echo "    -T ADDR      startup process wrapper, with socket address"
     2.5    echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
     2.6    echo "    -e MLTEXT    pass MLTEXT to the ML session"
     2.7 -  echo "    -f           pass 'Session.finish();' to the ML session"
     2.8    echo "    -m MODE      add print mode for output"
     2.9    echo "    -q           non-interactive session"
    2.10    echo "    -r           open heap file read-only"
    2.11 -  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    2.12    echo "    -w           reset write permissions on OUTPUT"
    2.13    echo
    2.14    echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
    2.15 @@ -69,7 +67,7 @@
    2.16  READONLY=""
    2.17  NOWRITE=""
    2.18  
    2.19 -while getopts "IPST:W:e:fm:qruw" OPT
    2.20 +while getopts "IPST:W:e:m:qrw" OPT
    2.21  do
    2.22    case "$OPT" in
    2.23      I)
    2.24 @@ -90,9 +88,6 @@
    2.25      e)
    2.26        MLTEXT="$MLTEXT $OPTARG"
    2.27        ;;
    2.28 -    f)
    2.29 -      MLTEXT="$MLTEXT Command_Line.tool0 Session.finish;"
    2.30 -      ;;
    2.31      m)
    2.32        if [ -z "$MODES" ]; then
    2.33          MODES="\"$OPTARG\""
    2.34 @@ -106,9 +101,6 @@
    2.35      r)
    2.36        READONLY=true
    2.37        ;;
    2.38 -    u)
    2.39 -      MLTEXT="$MLTEXT use\"ROOT.ML\";"
    2.40 -      ;;
    2.41      w)
    2.42        NOWRITE=true
    2.43        ;;
     3.1 --- a/src/Doc/System/Basics.thy	Fri May 17 18:23:39 2013 +0200
     3.2 +++ b/src/Doc/System/Basics.thy	Fri May 17 18:39:49 2013 +0200
     3.3 @@ -378,11 +378,9 @@
     3.4      -T ADDR      startup process wrapper, with socket address
     3.5      -W IN:OUT    startup process wrapper, with input/output fifos
     3.6      -e MLTEXT    pass MLTEXT to the ML session
     3.7 -    -f           pass 'Session.finish();' to the ML session
     3.8      -m MODE      add print mode for output
     3.9      -q           non-interactive session
    3.10      -r           open heap file read-only
    3.11 -    -u           pass 'use"ROOT.ML";' to the ML session
    3.12      -w           reset write permissions on OUTPUT
    3.13  
    3.14    INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
    3.15 @@ -430,12 +428,6 @@
    3.16    may happen when errorneous ML code is provided. Also make sure that
    3.17    the ML commands are terminated properly by semicolon.
    3.18  
    3.19 -  \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
    3.20 -  "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
    3.21 -  The @{verbatim "-f"} option passes ``@{verbatim
    3.22 -  "Session.finish();"}'', which is intended mainly for administrative
    3.23 -  purposes.
    3.24 -
    3.25    \medskip The @{verbatim "-m"} option adds identifiers of print modes
    3.26    to be made active for this session. Typically, this is used by some
    3.27    user interface, e.g.\ to enable output of proper mathematical
     4.1 --- a/src/Pure/build	Fri May 17 18:23:39 2013 +0200
     4.2 +++ b/src/Pure/build	Fri May 17 18:39:49 2013 +0200
     4.3 @@ -79,7 +79,8 @@
     4.4      "$ISABELLE_PROCESS" \
     4.5        -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
     4.6        -e "ml_prompts \"ML> \" \"ML# \";" \
     4.7 -      -f -q -w RAW_ML_SYSTEM "$OUTPUT"
     4.8 +      -e "Command_Line.tool0 Session.finish;" \
     4.9 +      -q -w RAW_ML_SYSTEM "$OUTPUT"
    4.10    fi
    4.11  fi
    4.12