# HG changeset patch # User wenzelm # Date 883577991 -3600 # Node ID 4a2c872b6513b1f345ae47dce8068d929faed8d6 # Parent 2f39aa4bebf3e4e9182b03104e3c6509508b3ad2 use feeder to pipe into ML; cleaned up; diff -r 2f39aa4bebf3 -r 4a2c872b6513 lib/scripts/run-mlworks --- a/lib/scripts/run-mlworks Wed Dec 31 15:17:49 1997 +0100 +++ b/lib/scripts/run-mlworks Wed Dec 31 15:19:51 1997 +0100 @@ -17,44 +17,39 @@ } -## basic setup - -EXIT="fun exit 0 : unit = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" -COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);" -COMMIT_RO='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\\n"); false);' - - ## prepare databases if [ -z "$INFILE" ]; then + EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" MLWORKS="mlworks-basis -tty" else + EXIT="" MLWORKS="mlimage -load $INFILE -tty" - EXIT="" fi -[ -z "$OUTFILE" ] && COMMIT="$COMMIT_RO" -[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } - -MLTEXT="$EXIT $COMMIT $MLTEXT" -MLEXIT="commit ();" +if [ -z "$OUTFILE" ]; then + COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' +else + COMMIT="fun commit () = (Shell.saveImage (\"$OUTFILE\", false); true);" + [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } +fi ## run it! -START_MLWORKS="$ML_HOME/$MLWORKS 2>&1 $ML_OPTIONS" +MLTEXT="$EXIT $COMMIT $MLTEXT" +MLEXIT="commit();" -if [ -n "$TERMINATE" ]; then - sh -c "echo '$MLTEXT' '$MLEXIT' | $START_MLWORKS" - RC=$? -elif [ -z "$MLTEXT" ]; then - sh -c "{ $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS" - RC=$? +if [ -z "$TERMINATE" ]; then + FEEDER_OPTS="-s" else - sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS" - RC=$? + FEEDER_OPTS="-q" fi -[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" +$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ + { read FPID; $ML_HOME/$MLWORKS $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; } +RC=$? + +[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" exit $RC diff -r 2f39aa4bebf3 -r 4a2c872b6513 lib/scripts/run-polyml --- 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 diff -r 2f39aa4bebf3 -r 4a2c872b6513 lib/scripts/run-smlnj --- a/lib/scripts/run-smlnj Wed Dec 31 15:17:49 1997 +0100 +++ b/lib/scripts/run-smlnj Wed Dec 31 15:19:51 1997 +0100 @@ -2,7 +2,7 @@ # # $Id$ # -# SML/NJ startup script (for 109.27 or later). +# SML/NJ startup script (for 109.27-109.33, 110 or later). # # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, # and from settings @@ -17,50 +17,49 @@ } -## basic setup - -EXIT="fun exit 0 : unit = OS.Process.exit OS.Process.success | exit _ = OS.Process.exit OS.Process.failure;" -COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");" -COMMIT_RO='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\\n"); false);' -eval $($ML_HOME/.arch-n-opsys) -SUFFIX=".$ARCH-$OPSYS" - - ## prepare databases -DB="$INFILE" - -if [ -n "$DB" ]; then +if [ -z "$INFILE" ]; then + EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" + DB="" +else + EXIT="" DB="@SMLload=$INFILE" - EXIT="" fi -[ -z "$OUTFILE" ] && COMMIT="$COMMIT_RO" -[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } - -MLTEXT="$EXIT $COMMIT $MLTEXT" -MLEXIT="commit ();" +if [ -z "$OUTFILE" ]; then + COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' +else + COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");" + [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } +fi ## run it! -START_SML="$ML_HOME/sml $ML_OPTIONS $DB" +MLTEXT="$EXIT $COMMIT $MLTEXT" +MLEXIT="commit();" -if [ -n "$TERMINATE" ]; then - sh -c "echo '$MLTEXT' '$MLEXIT' | $START_SML" - RC=$? -elif [ -z "$MLTEXT" ]; then - sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" - RC=$? +if [ -z "$TERMINATE" ]; then + FEEDER_OPTS="" else - sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML" - RC=$? + FEEDER_OPTS="-q" fi -#fix heap file name -[ -n "$OUTFILE" -a -n "$SUFFIX" -a -f "$OUTFILE$SUFFIX" ] \ - && mv "$OUTFILE$SUFFIX" "$OUTFILE" +$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ + { read FPID; $ML_HOME/sml $ML_OPTIONS $DB; RC=$?; kill -HUP $FPID; exit $RC; } +RC=$? + + +## fix heap file name and permissions -[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" +if [ -n "$OUTFILE" ]; then + eval $($ML_HOME/.arch-n-opsys) + SUFFIX=".$ARCH-$OPSYS" + if [ -f "$OUTFILE$SUFFIX" ]; then + mv "$OUTFILE$SUFFIX" "$OUTFILE" + [ -n "$NOWRITE" ] && chmod -w "$OUTFILE" + fi +fi exit $RC