bin/isabelle_process
changeset 58846 98c03412079b
parent 58842 22b87ab47d3b
child 59350 acba5d6fdb2f
--- a/bin/isabelle_process	Fri Oct 31 15:15:10 2014 +0100
+++ b/bin/isabelle_process	Fri Oct 31 16:03:45 2014 +0100
@@ -26,7 +26,6 @@
   echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
   echo
   echo "  Options are:"
-  echo "    -I           startup Isar interaction mode"
   echo "    -O           system options from given YXML file"
   echo "    -S           secure mode -- disallow critical operations"
   echo "    -T ADDR      startup process wrapper, with socket address"
@@ -57,7 +56,6 @@
 
 # options
 
-ISAR=""
 OPTIONS_FILE=""
 SECURE=""
 WRAPPER_SOCKET=""
@@ -69,12 +67,9 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "IO:ST:W:e:m:o:qrw" OPT
+while getopts "O:ST:W:e:m:o:qrw" OPT
 do
   case "$OPT" in
-    I)
-      ISAR=true
-      ;;
     O)
       OPTIONS_FILE="$OPTARG"
       ;;
@@ -208,8 +203,6 @@
 
 [ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
 
-NICE="nice"
-
 if [ -n "$WRAPPER_SOCKET" ]; then
   MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
 elif [ -n "$WRAPPER_FIFOS" ]; then
@@ -232,19 +225,14 @@
   if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
     MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
   fi
-  if [ -n "$ISAR" ]; then
-    MLTEXT="$MLTEXT; Isar.main ();"
-  else
-    NICE=""
-  fi
 fi
 
 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
 
 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
-  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
 else
-  $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
 fi
 RC="$?"