lib/scripts/run-smlnj
author wenzelm
Mon, 22 Jun 1998 15:25:06 +0200
changeset 5063 d45ec8d00ab0
parent 4505 4a2c872b6513
child 5708 fb09ab6a447f
permissions -rwxr-xr-x
check_mlhome_file;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2302
     2
#
wenzelm@2313
     3
# $Id$
wenzelm@2313
     4
#
wenzelm@4505
     5
# SML/NJ startup script (for 109.27-109.33, 110 or later).
wenzelm@2302
     6
#
wenzelm@4333
     7
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
wenzelm@2302
     8
# and from settings
wenzelm@2302
     9
wenzelm@2302
    10
wenzelm@2302
    11
## diagnostics
wenzelm@2302
    12
wenzelm@2349
    13
function fail_out()
wenzelm@2302
    14
{
wenzelm@2349
    15
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@2302
    16
  exit 2
wenzelm@2302
    17
}
wenzelm@2302
    18
wenzelm@5063
    19
function check_mlhome_file()
wenzelm@5063
    20
{
wenzelm@5063
    21
  if [ ! -f "$1" ]; then
wenzelm@5063
    22
    echo "Unable to locate $1" >&2
wenzelm@5063
    23
    echo "Please check your ML_HOME setting!" >&2
wenzelm@5063
    24
    exit 2
wenzelm@5063
    25
  fi
wenzelm@5063
    26
}
wenzelm@5063
    27
wenzelm@5063
    28
wenzelm@5063
    29
## compiler binaries
wenzelm@5063
    30
wenzelm@5063
    31
SML="$ML_HOME/sml"
wenzelm@5063
    32
ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
wenzelm@5063
    33
wenzelm@5063
    34
check_mlhome_file "$SML"
wenzelm@5063
    35
check_mlhome_file "$ARCH_N_OPSYS"
wenzelm@5063
    36
wenzelm@5063
    37
wenzelm@2302
    38
wenzelm@2302
    39
## prepare databases
wenzelm@2302
    40
wenzelm@4505
    41
if [ -z "$INFILE" ]; then
wenzelm@4505
    42
  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@4505
    43
  DB=""
wenzelm@4505
    44
else
wenzelm@4505
    45
  EXIT=""
wenzelm@3046
    46
  DB="@SMLload=$INFILE"
wenzelm@2349
    47
fi
wenzelm@2349
    48
wenzelm@4505
    49
if [ -z "$OUTFILE" ]; then
wenzelm@4505
    50
  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
wenzelm@4505
    51
else
wenzelm@4505
    52
  COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
wenzelm@4505
    53
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@4505
    54
fi
wenzelm@2302
    55
wenzelm@2302
    56
wenzelm@2302
    57
## run it!
wenzelm@2302
    58
wenzelm@4505
    59
MLTEXT="$EXIT $COMMIT $MLTEXT"
wenzelm@4505
    60
MLEXIT="commit();"
wenzelm@2302
    61
wenzelm@4505
    62
if [ -z "$TERMINATE" ]; then
wenzelm@4505
    63
  FEEDER_OPTS=""
wenzelm@2302
    64
else
wenzelm@4505
    65
  FEEDER_OPTS="-q"
wenzelm@2302
    66
fi
wenzelm@2302
    67
wenzelm@4505
    68
$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@5063
    69
  { read FPID; $SML $ML_OPTIONS $DB; RC=$?; kill -HUP $FPID; exit $RC; }
wenzelm@4505
    70
RC=$?
wenzelm@3046
    71
wenzelm@4505
    72
wenzelm@4505
    73
## fix heap file name and permissions
wenzelm@4505
    74
wenzelm@4505
    75
if [ -n "$OUTFILE" ]; then
wenzelm@5063
    76
  eval $($ARCH_N_OPSYS)
wenzelm@4505
    77
  SUFFIX=".$ARCH-$OPSYS"
wenzelm@4505
    78
  if [ -f "$OUTFILE$SUFFIX" ]; then
wenzelm@4505
    79
    mv "$OUTFILE$SUFFIX" "$OUTFILE"
wenzelm@4505
    80
    [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@4505
    81
  fi
wenzelm@4505
    82
fi
wenzelm@3503
    83
wenzelm@2302
    84
exit $RC