lib/scripts/run-smlnj
author wenzelm
Wed, 04 Dec 1996 13:05:47 +0100
changeset 2307 508d2a233dbc
parent 2302 47e078e60ab1
child 2313 d97eef398257
permissions -rwxr-xr-x
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     1
#!/bin/bash
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     2
#
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     3
# SML/NJ startup script (for 1.06 or later).
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     4
#
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     5
# $Id$
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     6
#
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     7
# Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE,
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     8
# and from settings
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     9
#
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    10
# MMW 30-Nov-1996
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    11
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    12
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    13
## diagnostics
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    14
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    15
function fail()
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    16
{
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    17
  echo "$1"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    18
  exit 2
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    19
}
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    20
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    21
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    22
## locations and settings
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    23
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    24
SML="$ML_HOME/bin/sml"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    25
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    26
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    27
## prepare databases
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    28
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    29
function fail_out()
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    30
{
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    31
  fail "Unable to create output heap file: \"$OUTFILE\""
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    32
}
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    33
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    34
if [ -z "$OUTFILE" ]; then
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    35
  DB="$INFILE"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    36
  COMMIT="fun commit() = output (std_out, \"Error - Database is not opened for writing.\\n\");"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    37
elif [ -n "$INFILE" -a "$INFILE" != "$OUTFILE" ]; then           # FIXME ! -ef !?
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    38
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    39
  cp "$INFILE" "$OUTFILE" || fail_out
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    40
  chmod +w "$OUTFILE"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    41
  DB="$INFILE"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    42
  COMMIT="fun commit() = (exportML\"$OUTFILE\"; ());"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    43
else
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    44
  DB="$INFILE"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    45
  COMMIT="fun commit() = (exportML\"$OUTFILE\"; ());"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    46
fi
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    47
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    48
[ -n "$DB" ] && DB="@SMLload=$DB"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    49
MLTEXT="$COMMIT $MLTEXT"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    50
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    51
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    52
## run it!
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    53
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    54
START_SML="$SML $ML_OPTIONS $OPTIONS $DB"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    55
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    56
if [ -n "$TERMINATE" ]; then
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    57
  echo "$MLTEXT" | $START_SML
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    58
  RC=$?
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    59
elif [ -z "$MLTEXT" ]; then
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    60
  $START_SML
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    61
  RC=$?
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    62
else
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    63
  TMP_FILE=/tmp/mltext-$$
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    64
  echo "$MLTEXT" >$TMP_FILE
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    65
  cat $TMP_FILE - | $START_SML
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    66
  RC=$?
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    67
  rm $TMP_FILE
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    68
fi
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    69
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    70
exit $RC