lib/scripts/run-smlnj-0.93
author wenzelm
Fri, 25 Apr 1997 15:10:52 +0200
changeset 3055 5da4afa207ad
parent 3010 4be22c300966
child 3503 390093b95cb0
permissions -rwxr-xr-x
removed COPYDB flag;
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
#
3055
5da4afa207ad removed COPYDB flag;
wenzelm
parents: 3010
diff changeset
     7
# Global vars: INFILE OUTFILE MLTEXT TERMINATE,
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"
b3ac45aba238 fixed EXIT def;
wenzelm
parents: 2411
diff changeset
    24
  EXIT="val exit = System.Unsafe.CInterface.exit;"
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
2622
80a81a36dd81 semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents: 2551
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
MLTEXT="$EXIT $COMMIT $MLTEXT"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    45
MLEXIT="commit();"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    46
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
## run it!
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    49
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    50
START_SML="$INFILE $ML_OPTIONS"
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    51
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    52
if [ -n "$TERMINATE" ]; then
3010
4be22c300966 fixed bash-2.0 problem;
wenzelm
parents: 3007
diff changeset
    53
  echo "$MLTEXT" "$MLEXIT" | $START_SML
2622
80a81a36dd81 semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents: 2551
diff changeset
    54
  RC=$?
80a81a36dd81 semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents: 2551
diff changeset
    55
elif [ -z "$MLTEXT" ]; then
80a81a36dd81 semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents: 2551
diff changeset
    56
  sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    57
  RC=$?
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    58
else
2622
80a81a36dd81 semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents: 2551
diff changeset
    59
  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    60
  RC=$?
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    61
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    62
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    63
if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
2551
fe15e3fcccf0 'rm -f' instead of 'mv -f';
wenzelm
parents: 2440
diff changeset
    64
  rm -f "$INFILE" || fail_out
fe15e3fcccf0 'rm -f' instead of 'mv -f';
wenzelm
parents: 2440
diff changeset
    65
  mv "$OUTFILE" "$INFILE" || fail_out
2411
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    66
fi
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    67
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    68
exit $RC