lib/scripts/run-smlnj-0.93
author wenzelm
Mon, 16 Dec 1996 10:29:30 +0100
changeset 2411 256dbda3df4f
child 2440 b3ac45aba238
permissions -rwxr-xr-x
SML/NJ startup script (for 0.93).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     1
#!/bin/bash -norc
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     2
#
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     3
# $Id$
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     4
#
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     5
# SML/NJ startup script (for 0.93).
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     6
#
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     7
# Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE,
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     8
# and from settings
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
     9
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    10
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    11
## diagnostics
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    12
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    13
function fail_out()
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    14
{
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    15
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    16
  exit 2
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    17
}
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    18
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    19
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    20
## prepare databases
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    21
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    22
EXIT="val exit = System.Unsafe.CInterface.exit;"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    23
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    24
[ -z "$INFILE" ] && INFILE="$ML_HOME/sml"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    25
MOVE=""
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    26
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    27
if [ -z "$OUTFILE" ]; then
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    28
  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    29
else
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    30
  if [ "$INFILE" -ef "$OUTFILE" ]; then
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    31
    OUTDIR=$(dirname "$OUTFILE")/tmp
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    32
    OUTFILE=$OUTDIR/$(basename "$OUTFILE")
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    33
    mkdir -p "$OUTDIR" || fail_out
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    34
    MOVE=true
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    35
  fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    36
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    37
  COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    38
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    39
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    40
MLTEXT="$EXIT $COMMIT $MLTEXT"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    41
MLEXIT="commit();"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    42
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    43
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    44
## run it!
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    45
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    46
START_SML="$INFILE $ML_OPTIONS"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    47
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    48
if [ -n "$TERMINATE" ]; then
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    49
  { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    50
  RC=$?
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    51
else
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    52
  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    53
  RC=$?
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    54
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    55
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    56
if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    57
  mv -f "$OUTFILE" "$INFILE" || fail_out
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    58
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    59
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    60
exit $RC