lib/scripts/run-polyml-5.0
changeset 21713 85722dc0fc81
parent 21711 dfac729d3066
child 21736 ccb2346ee416
equal deleted inserted replaced
21712:8b2fd895a7fc 21713:85722dc0fc81
    42 
    42 
    43 
    43 
    44 ## prepare databases
    44 ## prepare databases
    45 
    45 
    46 if [ -z "$INFILE" ]; then
    46 if [ -z "$INFILE" ]; then
       
    47   PRG="$POLY"
    47   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    48   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    48 else
    49 else
    49   check_file "$INFILE"
    50   check_file "$INFILE"
    50   POLY="$INFILE"
    51   PRG="$INFILE"
    51   EXIT=""
    52   EXIT=""
    52 fi
    53 fi
    53 
    54 
    54 ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
    55 ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
    55 
    56 
    75   FEEDER_OPTS=""
    76   FEEDER_OPTS=""
    76 else
    77 else
    77   FEEDER_OPTS="-q"
    78   FEEDER_OPTS="-q"
    78 fi
    79 fi
    79 
    80 
    80 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    81 if [ "$PRG" = "$POLY" ]; then
    81   { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    82   "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
       
    83     { read FPID; "$PRG" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
       
    84 else
       
    85   "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
       
    86     { read FPID; "$PRG" $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
       
    87 fi
    82 RC="$?"
    88 RC="$?"
    83 
    89 
    84 if [ -n "$OUTFILE" ]; then
    90 if [ -n "$OUTFILE" ]; then
    85   if [ -e "${OUTFILE}.o" ]; then
    91   if [ -e "${OUTFILE}.o" ]; then
    86     cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
    92     cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out