diff -r 83060e826e02 -r fafb8dfab7f6 lib/scripts/run-mosml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-mosml	Thu Jul 06 00:09:12 2000 +0200
@@ -0,0 +1,58 @@
+#!/bin/bash
+#
+# $Id$
+#
+# Moscow ML 2.00 startup script
+#
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
+# and from settings
+
+
+## diagnostics
+
+function fail_out()
+{
+  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
+  exit 2
+}
+
+
+## prepare databases
+
+MOSML="mosml -P sml90"
+
+if [ -z "$INFILE" ]; then
+  EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;'
+else
+  EXIT=""
+  echo "Cannot load images yet!" >&2
+  exit 2
+fi
+
+if [ -z "$OUTFILE" ]; then
+  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
+else
+  COMMIT="fun commit () = true;"
+  echo "WARNING: cannot save images yet!" >&2
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+fi
+
+
+## run it!
+
+MLTEXT="$EXIT $COMMIT $MLTEXT"
+MLEXIT="commit();"
+
+if [ -z "$TERMINATE" ]; then
+  FEEDER_OPTS=""
+else
+  FEEDER_OPTS="-q"
+fi
+
+$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; $ML_HOME/$MOSML $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
+RC=$?
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit $RC