lib/scripts/run-smlnj-0.93
author wenzelm
Fri, 02 Jan 1998 18:40:30 +0100
changeset 4513 6de428eac512
parent 4333 1d326b826851
child 5063 d45ec8d00ab0
permissions -rwxr-xr-x
feeder;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2936
diff changeset
     1
#!/bin/bash
2411
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
#
4333
1d326b826851 ISABELLE_TMP;
wenzelm
parents: 3503
diff changeset
     7
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
2411
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
2440
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    22
if [ -z "$INFILE" ]; then
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    23
  INFILE="$ML_HOME/sml"
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    24
  EXIT="val exit: int -> unit = System.Unsafe.CInterface.exit;"
2440
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    25
else
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    26
  EXIT=""
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    27
fi
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    28
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    29
MOVE=""
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    30
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    31
if [ -z "$OUTFILE" ]; then
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    32
  COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    33
else
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    34
  if [ "$INFILE" -ef "$OUTFILE" ]; then
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    35
    OUTDIR=$(dirname "$OUTFILE")/tmp
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    36
    OUTFILE=$OUTDIR/$(basename "$OUTFILE")
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    37
    mkdir -p "$OUTDIR" || fail_out
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    38
    MOVE=true
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    39
  fi
2936
bd33e7aae062 fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents: 2622
diff changeset
    40
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    41
  COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    42
fi
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
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    45
## run it!
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    46
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    47
MLTEXT="$EXIT $COMMIT $MLTEXT"
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    48
MLEXIT="commit();"
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    49
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    50
if [ -z "$TERMINATE" ]; then
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    51
  FEEDER_OPTS=""
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    52
else
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    53
  FEEDER_OPTS="-q"
2411
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
4513
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    56
$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    57
  { read FPID; $INFILE $ML_OPTIONS; RC=$?; kill -HUP $FPID; exit $RC; }
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    58
RC=$?
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    59
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    60
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    61
## fix heap file
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    62
6de428eac512 feeder;
wenzelm
parents: 4333
diff changeset
    63
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
3503
390093b95cb0 NOWRITE;
wenzelm
parents: 3055
diff changeset
    64
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    65
if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
2551
fe15e3fcccf0 'rm -f' instead of 'mv -f';
wenzelm
parents: 2440
diff changeset
    66
  rm -f "$INFILE" || fail_out
fe15e3fcccf0 'rm -f' instead of 'mv -f';
wenzelm
parents: 2440
diff changeset
    67
  mv "$OUTFILE" "$INFILE" || fail_out
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    68
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    69
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    70
exit $RC