lib/scripts/run-smlnj
author wenzelm
Tue, 17 Dec 1996 12:52:33 +0100
changeset 2429 747177b67670
parent 2396 721a9e01457b
child 2622 80a81a36dd81
permissions -rwxr-xr-x
fixed ML_HOME; chmod fix;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
     1
#!/bin/bash -norc
2302
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
#
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
     7
# Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE,
2302
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
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    13
function fail_out()
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    14
{
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    15
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
2302
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
## prepare databases
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    21
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    22
EXIT=""
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    23
if [ -z "$INFILE" ]; then
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    24
  case "$ML_SYSTEM" in
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    25
    smlnj-1.0[678])
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    26
      EXIT="val exit = System.Unix.exit;"
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    27
      ;;
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    28
    smlnj-1.09*)
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    29
      EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit _ = OS.Process.exit OS.Process.failure;"
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    30
    ;;
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    31
  esac
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    32
fi
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    33
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    34
DB="$INFILE"
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    35
[ -n "$DB" ] && DB="@SMLload=$INFILE"
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    36
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    37
COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    38
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    39
if [ -z "$OUTFILE" ]; then
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    40
  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    41
elif [ -n "$INFILE" -a ! "$INFILE" -ef "$OUTFILE" ]; then
2302
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    42
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    43
  cp "$INFILE" "$OUTFILE" || fail_out
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
2429
747177b67670 fixed ML_HOME;
wenzelm
parents: 2396
diff changeset
    46
[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
2396
721a9e01457b minor tuning;
wenzelm
parents: 2349
diff changeset
    47
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    48
MLTEXT="$EXIT $COMMIT $MLTEXT"
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    49
MLEXIT="commit();"
2302
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
2429
747177b67670 fixed ML_HOME;
wenzelm
parents: 2396
diff changeset
    54
START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
2302
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
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    57
  { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
2302
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
else
2349
e9475a7be4ad various fixes;
wenzelm
parents: 2316
diff changeset
    60
  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
2302
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
fi
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    63
47e078e60ab1 run-smlnj: SML/NJ startup script (for 1.06 or later).
wenzelm
parents:
diff changeset
    64
exit $RC