diff -r c567f9fd61a2 -r 1b2683e18fd2 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Sun Jun 05 11:31:16 2005 +0200
+++ b/lib/scripts/run-polyml	Sun Jun 05 11:31:17 2005 +0200
@@ -28,7 +28,6 @@
 
 ## Poly/ML programs
 
-FEEDER=""
 ML_DBASE_PREFIX=""
 POLY="$ML_HOME/poly"
 check_file "$POLY"
@@ -50,12 +49,18 @@
 
     DISCGARB="$POLY"
     DISCGARB_OPTIONS="-d -c"
+    case "$ML_SYSTEM" in
+      polyml-4.1.[12])
+	DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
+	;;
+      polyml-4.1.*)
+	DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
+	;;
+    esac
 
     EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
     ;;
   *)
-    FEEDER=true
-
     if [ -z "$ML_DBASE" ]; then
       ML_DBASE="$ML_HOME/ML_dbase"
     fi
@@ -72,14 +77,9 @@
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
-  FEEDER=true
   check_file "$ML_DBASE_PREFIX$ML_DBASE"
   INFILE="$ML_DBASE"
   MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
-  [ "$ML_SYSTEM" = polyml-4.1.3 ] && \
-    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
-  [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \
-    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
 else
   COPYDB=true
 fi
@@ -104,20 +104,18 @@
 
 ## run it!
 
+if [ -z "$TERMINATE" ]; then
+  FEEDER_OPTS=""
+else
+  FEEDER_OPTS="-q"
+fi
+
 DB_INFO=$(ls -l "$DB" 2>/dev/null)
 
-if [ -n "$TERMINATE" ]; then
-  echo "$MLTEXT" | "$POLY" $ML_OPTIONS "$DB"
-elif [ -n "$FEEDER" ]; then
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" | \
-    { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-else
-  "$POLY" $ML_OPTIONS "$DB" -- "$MLTEXT"
-fi
-
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
+  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"
 
-
 NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
   "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"