more careful evaluation of ML text, prevents spurious output;

--- a/lib/scripts/run-polyml-5.0	Fri Dec 08 23:25:50 2006 +0100
+++ b/lib/scripts/run-polyml-5.0	Fri Dec 08 23:25:52 2006 +0100
@@ -44,10 +44,11 @@
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
+  PRG="$POLY"
   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
 else
   check_file "$INFILE"
-  POLY="$INFILE"
+  PRG="$INFILE"
   EXIT=""
 fi
 
@@ -77,8 +78,13 @@
   FEEDER_OPTS="-q"
 fi
 
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+if [ "$PRG" = "$POLY" ]; then
+  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+    { read FPID; "$PRG" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+else
+  "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
+    { read FPID; "$PRG" $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+fi
 RC="$?"
 
 if [ -n "$OUTFILE" ]; then