bin/isabelle-process

   echo "    -P           startup Proof General interaction mode"
   echo "    -S           secure mode -- disallow critical operations"
   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."
   echo "  These are either names to be searched in the Isabelle path, or"
   echo "  actual file names (containing at least one /)."

 MODES=""
 TERMINATE=""
 READONLY=""
 NOWRITE=""
 
-while getopts "IPST:W:e:fm:qruw" OPT
+while getopts "IPST:W:e:m:qrw" OPT
 do
   case "$OPT" in
     I)
       ISAR=true
       ;;

     W)
       WRAPPER_FIFOS="$OPTARG"
       ;;
     e)
       MLTEXT="$MLTEXT $OPTARG"
-      ;;
-    f)
-      MLTEXT="$MLTEXT Command_Line.tool0 Session.finish;"
       ;;
     m)
       if [ -z "$MODES" ]; then
         MODES="\"$OPTARG\""
       else

     q)
       TERMINATE=true
       ;;
     r)
       READONLY=true
-      ;;
-    u)
-      MLTEXT="$MLTEXT use\"ROOT.ML\";"
       ;;
     w)
       NOWRITE=true
       ;;
     \?)