various fixes;

--- a/lib/scripts/run-polyml	Mon Dec 09 16:41:04 1996 +0100
+++ b/lib/scripts/run-polyml	Mon Dec 09 16:42:24 1996 +0100
@@ -1,88 +1,77 @@
-#!/bin/bash
+#!/bin/bash -norc
 #
 # $Id$
 #
 # Poly/ML startup script.
 #
-# Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE,
+# Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE,
 # and from settings
 
 
 ## diagnostics
 
-function fail()
+function fail_out()
 {
-  echo "$1"
+  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
   exit 2
 }
 
 
-
 ## locations and settings
 
-ML_QUIT=";PolyML.quit();"
 ML_DBASE=$ML_HOME/ML_dbase
 POLY=$ML_HOME/poly
 DISCGARB=$ML_HOME/discgarb
 
 case "$ML_SYSTEM" in
-  polyml-3.1)
+  polyml-3.*)
     DISCGARB="$DISCGARB -c"
-    export LM_LICENSE_FILE=$ML_HOME/license.dat
     ;;
 esac
 
 
-
 ## prepare databases
 
+MLINIT=""
+
 if [ -z "$INFILE" ]; then
   INFILE="$ML_DBASE"
-  MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT"
+  MLINIT="val use = PolyML.use; val exit = PolyML.exit; fun init_database () = ();"
 fi
 
-function fail_out()
-{
-  fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
 if [ -z "$OUTFILE" ]; then
   DB="$INFILE"
-  OPTS="-r"  
-elif [ "$INFILE" = "$OUTFILE" ]; then           # FIXME -ef !?
+  ML_OPTIONS="-r $ML_OPTIONS"  
+elif [ "$INFILE" -ef "$OUTFILE" ]; then
   DB="$INFILE"
-  OPTS=""
 elif [ -n "$COPYDB" ]; then
   cp "$INFILE" "$OUTFILE" || fail_out
-  chmod +w "$OUTFILE"
+  chmod +w "$OUTFILE" || fail_out
   DB="$OUTFILE"
-  OPTS=""
 else
   [ -f "$OUTFILE" ] && { rm "$OUTFILE" || fail_out }
-  echo "PolyML.make_database \"$OUTFILE\"; $ML_QUIT" | $POLY -r "$INFILE"
+  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
   [ -f "$OUTFILE" ] || fail_out
   DB="$OUTFILE"
-  OPTS=""
+  MLINIT="$MLINIT init_database ();"
 fi
 
 
-
 ## run it!
 
-START_POLY="$POLY $OPTS $ML_OPTIONS $OPTIONS $DB"
+START_POLY="$POLY $ML_OPTIONS $DB"
+
+[ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT"
 
 if [ -n "$TERMINATE" ]; then
-  echo "$MLTEXT" "$ML_QUIT" | $START_POLY
+  echo "$MLTEXT" | $START_POLY
   RC=$?
 elif [ -z "$MLTEXT" ]; then
   $START_POLY
   RC=$?
 else
-  TMP_FILE=/tmp/mltext-$$
-  echo "$MLTEXT" >$TMP_FILE
-  $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_POLY
+  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat } | $START_POLY
   RC=$?
-  rm $TMP_FILE
 fi
 
 [ $RC -eq 0 -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE"

--- a/lib/scripts/run-smlnj	Mon Dec 09 16:41:04 1996 +0100
+++ b/lib/scripts/run-smlnj	Mon Dec 09 16:42:24 1996 +0100
@@ -1,68 +1,63 @@
-#!/bin/bash
+#!/bin/bash -norc
 #
 # $Id$
 #
 # SML/NJ startup script (for 1.06 or later).
 #
-# Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE,
+# Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE,
 # and from settings
 
 
 ## diagnostics
 
-function fail()
+function fail_out()
 {
-  echo "$1"
+  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
   exit 2
 }
 
 
-## locations and settings
-
-SML="$ML_HOME/bin/sml"
-
-
 ## prepare databases
 
-function fail_out()
-{
-  fail "Unable to create output heap file: \"$OUTFILE\""
-}
+EXIT=""
+if [ -z "$INFILE" ]; then
+  case "$ML_SYSTEM" in
+    smlnj-1.0[678])
+      EXIT="val exit = System.Unix.exit;"
+      ;;
+    smlnj-1.09*)
+      EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit _ = OS.Process.exit OS.Process.failure;"
+    ;;
+  esac
+fi
+
+DB="$INFILE"
+[ -n "$DB" ] && DB="@SMLload=$INFILE"
+
+COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
 
 if [ -z "$OUTFILE" ]; then
-  DB="$INFILE"
-  COMMIT='fun commit() = (output (std_out, "Error - Database is not opened for writing.\n"); false);'
-elif [ -n "$INFILE" -a "$INFILE" != "$OUTFILE" ]; then           # FIXME ! -ef !?
+  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
+elif [ -n "$INFILE" -a ! "$INFILE" -ef "$OUTFILE" ]; then
   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
   cp "$INFILE" "$OUTFILE" || fail_out
-  chmod +w "$OUTFILE"
-  DB="$INFILE"
-  COMMIT="fun commit() = not (exportML\"$OUTFILE\");"
-else
-  DB="$INFILE"
-  COMMIT="fun commit() = not (exportML\"$OUTFILE\");"
+  chmod +w "$OUTFILE" || fail_out
 fi
 
-[ -n "$DB" ] && DB="@SMLload=$DB"
-MLTEXT="$COMMIT $MLTEXT"
+MLTEXT="$EXIT $COMMIT $MLTEXT"
+MLEXIT="commit();"
 
 
 ## run it!
 
-START_SML="$SML $ML_OPTIONS $OPTIONS $DB"
+START_SML="$ML_HOME/bin/sml $ML_OPTIONS $DB"
 
 if [ -n "$TERMINATE" ]; then
-  echo "$MLTEXT" | $START_SML
-  RC=$?
-elif [ -z "$MLTEXT" ]; then
-  $START_SML
+  { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
   RC=$?
 else
-  TMP_FILE=/tmp/mltext-$$
-  echo "$MLTEXT" >$TMP_FILE
-  $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_SML
+  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
   RC=$?
-  rm $TMP_FILE
 fi
 
 exit $RC