lib/scripts/run-polyml-5.5.1
author wenzelm
Thu Nov 13 23:45:15 2014 +0100 (2014-11-13)
changeset 58999 ed09ae4ea2d8
parent 56627 cb912b7de3cf
child 59344 e0ce214303c1
permissions -rwxr-xr-x
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;
     1 #!/usr/bin/env bash
     2 # :mode=shellscript:
     3 #
     4 # Author: Makarius
     5 #
     6 # Startup script for Poly/ML 5.5.1.
     7 
     8 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
     9 
    10 
    11 ## diagnostics
    12 
    13 function fail()
    14 {
    15   echo "$1" >&2
    16   exit 2
    17 }
    18 
    19 function fail_out()
    20 {
    21   fail "Unable to create output heap file: \"$OUTFILE\""
    22 }
    23 
    24 function check_file()
    25 {
    26   [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    27 }
    28 
    29 
    30 ## compiler executables and libraries
    31 
    32 [ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    33 
    34 POLY="$ML_HOME/poly"
    35 check_file "$POLY"
    36 
    37 librarypath "$ML_HOME"
    38 
    39 
    40 
    41 ## prepare databases
    42 
    43 if [ -z "$INFILE" ]; then
    44   INIT=""
    45   EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    46 else
    47   check_file "$INFILE"
    48   INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
    49   EXIT=""
    50 fi
    51 
    52 if [ -z "$OUTFILE" ]; then
    53   COMMIT='fun commit () = false;'
    54   MLEXIT=""
    55 else
    56   if [ -z "$INFILE" ]; then
    57     COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
    58   else
    59     COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
    60   fi
    61   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    62   MLEXIT="commit();"
    63 fi
    64 
    65 
    66 ## run it!
    67 
    68 MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
    69 
    70 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    71   "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    72     --error-exit </dev/null
    73   RC="$?"
    74 else
    75   if [ -z "$TERMINATE" ]; then
    76     FEEDER_OPTS=""
    77   else
    78     FEEDER_OPTS="-q"
    79     ML_OPTIONS="$ML_OPTIONS --error-exit"
    80   fi
    81   "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    82     { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    83   RC="$?"
    84 fi
    85 
    86 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    87 
    88 exit "$RC"
    89 
    90 #:wrap=soft:maxLineLen=100: