lib/scripts/run-smlnj
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 59344 e0ce214303c1
permissions -rwxr-xr-x
updated for release;
     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   MLEXIT=""
    66 else
    67   if [ -z "$INFILE" ]; then
    68     MLEXIT="if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
    69   else
    70     MLEXIT="Session.save \"$OUTFILE\";"
    71   fi
    72   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    73 fi
    74 
    75 
    76 ## run it!
    77 
    78 MLTEXT="$EXIT $MLTEXT"
    79 
    80 if [ -z "$TERMINATE" ]; then
    81   FEEDER_OPTS=""
    82 else
    83   FEEDER_OPTS="-q"
    84 fi
    85 
    86 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    87   { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    88 RC="$?"
    89 
    90 
    91 ## fix heap file name and permissions
    92 
    93 if [ -n "$OUTFILE" ]; then
    94   check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    95 fi
    96 
    97 exit "$RC"