lib/scripts/run-mosml
changeset 9253 fafb8dfab7f6
child 9789 7e5e6c47c0b5
equal deleted inserted replaced
9252:83060e826e02 9253:fafb8dfab7f6
       
     1 #!/bin/bash
       
     2 #
       
     3 # $Id$
       
     4 #
       
     5 # Moscow ML 2.00 startup script
       
     6 #
       
     7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
       
     8 # and from settings
       
     9 
       
    10 
       
    11 ## diagnostics
       
    12 
       
    13 function fail_out()
       
    14 {
       
    15   echo "Unable to create output heap file: \"$OUTFILE\"" >&2
       
    16   exit 2
       
    17 }
       
    18 
       
    19 
       
    20 ## prepare databases
       
    21 
       
    22 MOSML="mosml -P sml90"
       
    23 
       
    24 if [ -z "$INFILE" ]; then
       
    25   EXIT='load "OS"; fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;'
       
    26 else
       
    27   EXIT=""
       
    28   echo "Cannot load images yet!" >&2
       
    29   exit 2
       
    30 fi
       
    31 
       
    32 if [ -z "$OUTFILE" ]; then
       
    33   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
       
    34 else
       
    35   COMMIT="fun commit () = true;"
       
    36   echo "WARNING: cannot save images yet!" >&2
       
    37   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
       
    38 fi
       
    39 
       
    40 
       
    41 ## run it!
       
    42 
       
    43 MLTEXT="$EXIT $COMMIT $MLTEXT"
       
    44 MLEXIT="commit();"
       
    45 
       
    46 if [ -z "$TERMINATE" ]; then
       
    47   FEEDER_OPTS=""
       
    48 else
       
    49   FEEDER_OPTS="-q"
       
    50 fi
       
    51 
       
    52 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
       
    53   { read FPID; $ML_HOME/$MOSML $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
       
    54 RC=$?
       
    55 
       
    56 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
       
    57 
       
    58 exit $RC