lib/scripts/run-mlworks
changeset 9789 7e5e6c47c0b5
parent 4505 4a2c872b6513
child 9868 580c50fc6559
equal deleted inserted replaced
9788:df671fa2562a 9789:7e5e6c47c0b5
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     4 #
     6 #
     5 # MLWorks startup script (for 1.0r2 or later).
     7 # MLWorks startup script (for 1.0r2 or later).
     6 #
     8 #
     7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
     9 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
     8 # and from settings
    10 # and from settings
    22 if [ -z "$INFILE" ]; then
    24 if [ -z "$INFILE" ]; then
    23   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    25   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    24   MLWORKS="mlworks-basis -tty"
    26   MLWORKS="mlworks-basis -tty"
    25 else
    27 else
    26   EXIT=""
    28   EXIT=""
    27   MLWORKS="mlimage -load $INFILE -tty"
    29   MLWORKS="mlimage -load \"$INFILE\" -tty"
    28 fi
    30 fi
    29 
    31 
    30 if [ -z "$OUTFILE" ]; then
    32 if [ -z "$OUTFILE" ]; then
    31   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    33   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    32 else
    34 else
    44   FEEDER_OPTS="-s"
    46   FEEDER_OPTS="-s"
    45 else
    47 else
    46   FEEDER_OPTS="-q"
    48   FEEDER_OPTS="-q"
    47 fi
    49 fi
    48 
    50 
    49 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    51 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    50   { read FPID; $ML_HOME/$MLWORKS $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
    52   { read FPID; "$ML_HOME/$MLWORKS" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    51 RC=$?
    53 RC="$?"
    52 
    54 
    53 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    55 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    54 
    56 
    55 exit $RC
    57 exit "$RC"