lib/scripts/run-mosml
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 10105 f9be78009930
child 10555 2323ec838401
permissions -rwxr-xr-x
proper symbol markup with \isamath, \isatext; support sub/super scripts:
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
9977
32955afeb835 unexport exports;
wenzelm
parents: 9794
diff changeset
     8
10105
f9be78009930 added COPYDB argument;
wenzelm
parents: 9997
diff changeset
     9
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    10
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
## diagnostics
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    13
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    14
function fail_out()
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    15
{
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    16
  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
    17
  exit 2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    18
}
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
## prepare databases
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    22
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    23
MOSML="mosml -P sml90"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    24
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    25
if [ -z "$INFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    26
  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
    27
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    28
  EXIT=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    29
  echo "Cannot load images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    30
  exit 2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    31
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    32
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    33
if [ -z "$OUTFILE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    34
  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
    35
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    36
  COMMIT="fun commit () = true;"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    37
  echo "WARNING: cannot save images yet!" >&2
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    38
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    39
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    40
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
## run it!
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    43
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    44
MLTEXT="$EXIT $COMMIT $MLTEXT"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    45
MLEXIT="commit();"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    46
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    47
if [ -z "$TERMINATE" ]; then
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    48
  FEEDER_OPTS=""
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    49
else
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    50
  FEEDER_OPTS="-q"
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    51
fi
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    52
9789
wenzelm
parents: 9253
diff changeset
    53
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9789
diff changeset
    54
  { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
9789
wenzelm
parents: 9253
diff changeset
    55
RC="$?"
9253
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    56
fafb8dfab7f6 run Moscow ML 2.00 --- does not handle saved images (yet!?);
wenzelm
parents:
diff changeset
    57
[ -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
    58
9789
wenzelm
parents: 9253
diff changeset
    59
exit "$RC"