lib/scripts/run-smlnj
author nipkow
Wed Aug 26 19:54:19 2009 +0200 (2009-08-26)
changeset 32416 4ea7648b6ae2
parent 31317 1f5740424c69
child 39619 34952c2423c6
permissions -rwxr-xr-x
merged
     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_out()
    13 {
    14   echo "Unable to create output heap file: \"$OUTFILE\"" >&2
    15   exit 2
    16 }
    17 
    18 function check_mlhome_file()
    19 {
    20   if [ ! -f "$1" ]; then
    21     echo "Unable to locate $1" >&2
    22     echo "Please check your ML_HOME setting!" >&2
    23     exit 2
    24   fi
    25 }
    26 
    27 function check_heap_file()
    28 {
    29   if [ ! -f "$1" ]; then
    30     echo "Expected to find ML heap file $1" >&2
    31     return 1
    32   else
    33     return 0
    34   fi
    35 }
    36 
    37 
    38 
    39 ## compiler binaries
    40 
    41 SML="$ML_HOME/sml"
    42 ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
    43 
    44 check_mlhome_file "$SML"
    45 check_mlhome_file "$ARCH_N_OPSYS"
    46 
    47 
    48 
    49 ## prepare databases
    50 
    51 if [ -z "$INFILE" ]; then
    52   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    53   DB=""
    54 else
    55   EXIT=""
    56   DB="@SMLload=$INFILE"
    57 fi
    58 
    59 if [ -z "$OUTFILE" ]; then
    60   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    61 else
    62   COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
    63   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    64 fi
    65 
    66 
    67 ## run it!
    68 
    69 MLTEXT="$EXIT $COMMIT $MLTEXT"
    70 MLEXIT="commit();"
    71 
    72 if [ -z "$TERMINATE" ]; then
    73   FEEDER_OPTS=""
    74 else
    75   FEEDER_OPTS="-q"
    76 fi
    77 
    78 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    79   { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    80 RC="$?"
    81 
    82 
    83 ## fix heap file name and permissions
    84 
    85 if [ -n "$OUTFILE" ]; then
    86   eval $("$ARCH_N_OPSYS")
    87   [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
    88   HEAP="$OUTFILE.$HEAP_SUFFIX"
    89   check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
    90     [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    91 fi
    92 
    93 exit "$RC"