discontinued obsolete isabelle-process options -f and -u;

--- a/NEWS	Fri May 17 18:23:39 2013 +0200
+++ b/NEWS	Fri May 17 18:39:49 2013 +0200
@@ -235,6 +235,9 @@
 * Discontinued obsolete isabelle usedir, mkdir, make -- superseded by
 "isabelle build" in Isabelle2013.  INCOMPATIBILITY.
 
+* Discontinued obsolete isabelle-process options -f and -u (former
+administrative aliases of option -e).  Minor INCOMPATIBILITY.
+
 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
 specify global resources of the JVM process run by isabelle build.
 

--- a/bin/isabelle-process	Fri May 17 18:23:39 2013 +0200
+++ b/bin/isabelle-process	Fri May 17 18:39:49 2013 +0200
@@ -32,11 +32,9 @@
   echo "    -T ADDR      startup process wrapper, with socket address"
   echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
-  echo "    -f           pass 'Session.finish();' to the ML session"
   echo "    -m MODE      add print mode for output"
   echo "    -q           non-interactive session"
   echo "    -r           open heap file read-only"
-  echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
   echo "    -w           reset write permissions on OUTPUT"
   echo
   echo "  INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
@@ -69,7 +67,7 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "IPST:W:e:fm:qruw" OPT
+while getopts "IPST:W:e:m:qrw" OPT
 do
   case "$OPT" in
     I)
@@ -90,9 +88,6 @@
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;
-    f)
-      MLTEXT="$MLTEXT Command_Line.tool0 Session.finish;"
-      ;;
     m)
       if [ -z "$MODES" ]; then
         MODES="\"$OPTARG\""
@@ -106,9 +101,6 @@
     r)
       READONLY=true
       ;;
-    u)
-      MLTEXT="$MLTEXT use\"ROOT.ML\";"
-      ;;
     w)
       NOWRITE=true
       ;;

--- a/src/Doc/System/Basics.thy	Fri May 17 18:23:39 2013 +0200
+++ b/src/Doc/System/Basics.thy	Fri May 17 18:39:49 2013 +0200
@@ -378,11 +378,9 @@
     -T ADDR      startup process wrapper, with socket address
     -W IN:OUT    startup process wrapper, with input/output fifos
     -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
-    -u           pass 'use"ROOT.ML";' to the ML session
     -w           reset write permissions on OUTPUT
 
   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
@@ -430,12 +428,6 @@
   may happen when errorneous ML code is provided. Also make sure that
   the ML commands are terminated properly by semicolon.
 
-  \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
-  "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
-  The @{verbatim "-f"} option passes ``@{verbatim
-  "Session.finish();"}'', which is intended mainly for administrative
-  purposes.
-
   \medskip The @{verbatim "-m"} option adds identifiers of print modes
   to be made active for this session. Typically, this is used by some
   user interface, e.g.\ to enable output of proper mathematical

--- a/src/Pure/build	Fri May 17 18:23:39 2013 +0200
+++ b/src/Pure/build	Fri May 17 18:39:49 2013 +0200
@@ -79,7 +79,8 @@
     "$ISABELLE_PROCESS" \
       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
-      -f -q -w RAW_ML_SYSTEM "$OUTPUT"
+      -e "Command_Line.tool0 Session.finish;" \
+      -q -w RAW_ML_SYSTEM "$OUTPUT"
   fi
 fi