lib/scripts/run-smlnj-0.93
author wenzelm
Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754 59bd96046ad6
parent 2622 80a81a36dd81
child 2936 bd33e7aae062
permissions -rwxr-xr-x
moved settings comment to build;
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
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
256dbda3df4f SML/NJ startup script (for 0.93).
wenzelm
parents:
diff changeset
    40
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
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
2622
80a81a36dd81 semi fix of piping-quit peoblem (should work on systems with *real* sh);
wenzelm
parents: 2551
diff changeset
    53
  { echo "$MLTEXT" "$MLEXIT" } | $START_SML
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