lib/scripts/run-mosml
author nipkow
Wed Aug 26 19:54:19 2009 +0200 (2009-08-26)
changeset 32416 4ea7648b6ae2
parent 31317 1f5740424c69
permissions -rwxr-xr-x
merged
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@9253
     2
#
wenzelm@9789
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@9253
     4
#
wenzelm@9253
     5
# Moscow ML 2.00 startup script
wenzelm@9977
     6
wenzelm@31317
     7
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
wenzelm@9253
     8
wenzelm@9253
     9
wenzelm@9253
    10
## diagnostics
wenzelm@9253
    11
wenzelm@9253
    12
function fail_out()
wenzelm@9253
    13
{
wenzelm@9253
    14
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@9253
    15
  exit 2
wenzelm@9253
    16
}
wenzelm@9253
    17
wenzelm@9253
    18
wenzelm@9253
    19
## prepare databases
wenzelm@9253
    20
wenzelm@9253
    21
MOSML="mosml -P sml90"
wenzelm@9253
    22
wenzelm@9253
    23
if [ -z "$INFILE" ]; then
wenzelm@9253
    24
  EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;'
wenzelm@9253
    25
else
wenzelm@9253
    26
  EXIT=""
wenzelm@9253
    27
  echo "Cannot load images yet!" >&2
wenzelm@9253
    28
  exit 2
wenzelm@9253
    29
fi
wenzelm@9253
    30
wenzelm@9253
    31
if [ -z "$OUTFILE" ]; then
wenzelm@9253
    32
  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
wenzelm@9253
    33
else
wenzelm@9253
    34
  COMMIT="fun commit () = true;"
wenzelm@9253
    35
  echo "WARNING: cannot save images yet!" >&2
wenzelm@9253
    36
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@9253
    37
fi
wenzelm@9253
    38
wenzelm@9253
    39
wenzelm@9253
    40
## run it!
wenzelm@9253
    41
wenzelm@9253
    42
MLTEXT="$EXIT $COMMIT $MLTEXT"
wenzelm@9253
    43
MLEXIT="commit();"
wenzelm@9253
    44
wenzelm@9253
    45
if [ -z "$TERMINATE" ]; then
wenzelm@9253
    46
  FEEDER_OPTS=""
wenzelm@9253
    47
else
wenzelm@9253
    48
  FEEDER_OPTS="-q"
wenzelm@9253
    49
fi
wenzelm@9253
    50
wenzelm@9789
    51
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@9794
    52
  { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@9789
    53
RC="$?"
wenzelm@9253
    54
wenzelm@9253
    55
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@9253
    56
wenzelm@9789
    57
exit "$RC"