--- a/lib/scripts/run-polyml Wed Dec 31 15:17:49 1997 +0100
+++ b/lib/scripts/run-polyml Wed Dec 31 15:19:51 1997 +0100
@@ -59,22 +59,20 @@
## run it!
-START_POLY="$POLY $ML_OPTIONS $DB"
+if [ -z "$TERMINATE" ]; then
+ FEEDER_OPTS="-s"
+else
+ FEEDER_OPTS="-q"
+fi
+
DB_INFO=$(ls -l "$DB")
-if [ -n "$TERMINATE" ]; then
- echo "$MLTEXT" | $START_POLY
- RC=$?
-elif [ -z "$MLTEXT" ]; then
- sh -c "$ISABELLE_HOME/lib/Tools/symbolinput | $START_POLY"
- RC=$?
-else
- sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; } | $START_POLY"
- RC=$?
-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")
[ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
-[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
exit $RC