lib/scripts/run-smlnj
author wenzelm
Mon, 09 Dec 1996 16:39:53 +0100
changeset 2346 c0165f34e987
parent 2316 ba9c9ed28dd8
child 2349 e9475a7be4ad
permissions -rwxr-xr-x
getplatform - bash source script to augment current env;
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
#
2313
d97eef398257 replaced cat by ucat;
wenzelm
parents: 2302
diff changeset
     3
# $Id$
d97eef398257 replaced cat by ucat;
wenzelm
parents: 2302
diff changeset
     4
#
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
     5
# 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
     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
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    11
## diagnostics
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
function fail()
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
  echo "$1"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    16
  exit 2
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    17
}
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    18
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
## locations and settings
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
SML="$ML_HOME/bin/sml"
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
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    25
## prepare databases
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
function fail_out()
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
  fail "Unable to create output heap file: \"$OUTFILE\""
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
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    32
if [ -z "$OUTFILE" ]; then
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    33
  DB="$INFILE"
2316
ba9c9ed28dd8 fixed commit emulation;
wenzelm
parents: 2313
diff changeset
    34
  COMMIT='fun commit() = (output (std_out, "Error - Database is not opened for writing.\n"); false);'
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    35
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
    36
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    37
  cp "$INFILE" "$OUTFILE" || fail_out
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    38
  chmod +w "$OUTFILE"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    39
  DB="$INFILE"
2316
ba9c9ed28dd8 fixed commit emulation;
wenzelm
parents: 2313
diff changeset
    40
  COMMIT="fun commit() = not (exportML\"$OUTFILE\");"
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    41
else
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    42
  DB="$INFILE"
2316
ba9c9ed28dd8 fixed commit emulation;
wenzelm
parents: 2313
diff changeset
    43
  COMMIT="fun commit() = not (exportML\"$OUTFILE\");"
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    44
fi
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    45
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    46
[ -n "$DB" ] && DB="@SMLload=$DB"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    47
MLTEXT="$COMMIT $MLTEXT"
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    48
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    49
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    50
## run it!
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
START_SML="$SML $ML_OPTIONS $OPTIONS $DB"
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
if [ -n "$TERMINATE" ]; then
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    55
  echo "$MLTEXT" | $START_SML
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    56
  RC=$?
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    57
elif [ -z "$MLTEXT" ]; then
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    58
  $START_SML
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    59
  RC=$?
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    60
else
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    61
  TMP_FILE=/tmp/mltext-$$
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    62
  echo "$MLTEXT" >$TMP_FILE
2313
d97eef398257 replaced cat by ucat;
wenzelm
parents: 2302
diff changeset
    63
  $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_SML
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    64
  RC=$?
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    65
  rm $TMP_FILE
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    66
fi
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    67
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    68
exit $RC