# HG changeset patch
# User wenzelm
# Date 1197737612 -3600
# Node ID b2ed983a5e807ddb7281f9f81abf7af04455b33c
# Parent  d30391cdd9d9725ce6878571962f157295ea68b9
non-ML session: run with 'nice', to prevent isabelle process from flooding interactive front-ends (ProofGeneral/XEmacs etc.)

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="$?"