diff -r d30391cdd9d9 -r b2ed983a5e80 bin/isabelle-process --- a/bin/isabelle-process Sat Dec 15 14:52:55 2007 +0100 +++ b/bin/isabelle-process Sat Dec 15 17:53:32 2007 +0100 @@ -222,6 +222,7 @@ [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" +NICE="nice" if [ -n "$WRAPPER" ]; then MLTEXT="$MLTEXT; IsabelleProcess.init();" elif [ -n "$PGIP" ]; then @@ -230,15 +231,17 @@ MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" elif [ "$ISAR" = true ]; then MLTEXT="$MLTEXT; Isar.main();" +else + NICE="" fi export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \ ISABELLE_PID ISABELLE_TMP if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then - "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" + $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" else - "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" + $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" fi RC="$?"