# HG changeset patch
# User wenzelm
# Date 1114537916 -7200
# Node ID 30e878979457aba9f6631895973ea37b4ab8f593
# Parent  a2c8160b58fd4e5cae64f3ab17db4604d866ea27
no longer need feeder to run normal interactive sessions;

diff -r a2c8160b58fd -r 30e878979457 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Tue Apr 26 19:51:28 2005 +0200
+++ b/lib/scripts/run-polyml	Tue Apr 26 19:51:56 2005 +0200
@@ -28,6 +28,7 @@
 
 ## Poly/ML programs
 
+FEEDER=""
 ML_DBASE_PREFIX=""
 POLY="$ML_HOME/poly"
 check_file "$POLY"
@@ -53,6 +54,8 @@
     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
@@ -69,11 +72,12 @@
 ## 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 -Smax"
+    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
@@ -82,7 +86,7 @@
 
 if [ -z "$OUTFILE" ]; then
   DB="$INFILE"
-  ML_OPTIONS="-r $ML_OPTIONS"  
+  ML_OPTIONS="-r $ML_OPTIONS"
 elif [ "$INFILE" -ef "$OUTFILE" ]; then
   DB="$INFILE"
 elif [ -n "$COPYDB" ]; then
@@ -100,16 +104,17 @@
 
 ## run it!
 
-if [ -z "$TERMINATE" ]; then
-  FEEDER_OPTS=""
+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
-  FEEDER_OPTS="-q"
+  "$POLY" $ML_OPTIONS "$DB" -- "$MLTEXT"
 fi
 
-DB_INFO=$(ls -l "$DB" 2>/dev/null)
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
-  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"