lib/scripts/run-smlnj
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 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # SML/NJ startup script (for 110 or later).
     6 
     7 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
     8 
     9 
    10 ## diagnostics
    11 
    12 function fail()
    13 {
    14   echo "$1" >&2
    15   exit 2
    16 }
    17 
    18 function fail_out()
    19 {
    20   fail "Unable to create output heap file: \"$OUTFILE\""
    21 }
    22 
    23 function check_mlhome_file()
    24 {
    25   [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    26 }
    27 
    28 function check_heap_file()
    29 {
    30   if [ ! -f "$1" ]; then
    31     echo "Expected to find ML heap file $1" >&2
    32     return 1
    33   else
    34     return 0
    35   fi
    36 }
    37 
    38 
    39 
    40 ## compiler binaries
    41 
    42 [ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    43 
    44 SML="$ML_HOME/sml"
    45 ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
    46 
    47 check_mlhome_file "$SML"
    48 check_mlhome_file "$ARCH_N_OPSYS"
    49 
    50 eval $("$ARCH_N_OPSYS")
    51 
    52 
    53 
    54 ## prepare databases
    55 
    56 if [ -z "$INFILE" ]; then
    57   EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    58   DB=""
    59 else
    60   EXIT=""
    61   DB="@SMLload=$INFILE"
    62 fi
    63 
    64 if [ -z "$OUTFILE" ]; then
    65   COMMIT='fun commit () = false;'
    66   MLEXIT=""
    67 else
    68   if [ -z "$INFILE" ]; then
    69     COMMIT="fun commit () = if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
    70   else
    71     COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
    72   fi
    73   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    74   MLEXIT="commit();"
    75 fi
    76 
    77 
    78 ## run it!
    79 
    80 MLTEXT="$EXIT $COMMIT $MLTEXT"
    81 
    82 if [ -z "$TERMINATE" ]; then
    83   FEEDER_OPTS=""
    84 else
    85   FEEDER_OPTS="-q"
    86 fi
    87 
    88 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    89   { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    90 RC="$?"
    91 
    92 
    93 ## fix heap file name and permissions
    94 
    95 if [ -n "$OUTFILE" ]; then
    96   check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    97 fi
    98 
    99 exit "$RC"