lib/scripts/run-mosml
author wenzelm
Fri, 01 Sep 2000 19:42:11 +0200
changeset 9794 2be239143d42
parent 9789 7e5e6c47c0b5
child 9977 32955afeb835
permissions -rwxr-xr-x
fixed quoting;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     1
#!/bin/bash
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     2
#
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     3
# $Id$
9789
wenzelm
parents: 9253
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 9253
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     6
#
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     7
# Moscow ML 2.00 startup script
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     8
#
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
     9
# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    10
# and from settings
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    11
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    12
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    13
## diagnostics
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    14
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    15
function fail_out()
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    16
{
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    17
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    18
  exit 2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    19
}
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    20
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    21
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    22
## prepare databases
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    23
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    24
MOSML="mosml -P sml90"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    25
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    26
if [ -z "$INFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    27
  EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;'
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    28
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    29
  EXIT=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    30
  echo "Cannot load images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    31
  exit 2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    32
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    33
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    34
if [ -z "$OUTFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    35
  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    36
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    37
  COMMIT="fun commit () = true;"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    38
  echo "WARNING: cannot save images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    39
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    40
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    41
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    42
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    43
## run it!
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    44
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    45
MLTEXT="$EXIT $COMMIT $MLTEXT"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    46
MLEXIT="commit();"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    47
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    48
if [ -z "$TERMINATE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    49
  FEEDER_OPTS=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    50
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    51
  FEEDER_OPTS="-q"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    52
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    53
9789
wenzelm
parents: 9253
diff changeset
    54
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9789
diff changeset
    55
  { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
9789
wenzelm
parents: 9253
diff changeset
    56
RC="$?"
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    57
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    58
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    59
9789
wenzelm
parents: 9253
diff changeset
    60
exit "$RC"