lib/scripts/run-smlnj-0.93
changeset 2411 256dbda3df4f
child 2440 b3ac45aba238
equal deleted inserted replaced
2410:a0727e4d9453 2411:256dbda3df4f
       
     1 #!/bin/bash -norc
       
     2 #
       
     3 # $Id$
       
     4 #
       
     5 # SML/NJ startup script (for 0.93).
       
     6 #
       
     7 # Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE,
       
     8 # and from settings
       
     9 
       
    10 
       
    11 ## diagnostics
       
    12 
       
    13 function fail_out()
       
    14 {
       
    15   echo "Unable to create output heap file: \"$OUTFILE\"" >&2
       
    16   exit 2
       
    17 }
       
    18 
       
    19 
       
    20 ## prepare databases
       
    21 
       
    22 EXIT="val exit = System.Unsafe.CInterface.exit;"
       
    23 
       
    24 [ -z "$INFILE" ] && INFILE="$ML_HOME/sml"
       
    25 MOVE=""
       
    26 
       
    27 if [ -z "$OUTFILE" ]; then
       
    28   COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);'
       
    29 else
       
    30   if [ "$INFILE" -ef "$OUTFILE" ]; then
       
    31     OUTDIR=$(dirname "$OUTFILE")/tmp
       
    32     OUTFILE=$OUTDIR/$(basename "$OUTFILE")
       
    33     mkdir -p "$OUTDIR" || fail_out
       
    34     MOVE=true
       
    35   fi
       
    36   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
       
    37   COMMIT="fun commit () = not (exportML\"$OUTFILE\");"
       
    38 fi
       
    39 
       
    40 MLTEXT="$EXIT $COMMIT $MLTEXT"
       
    41 MLEXIT="commit();"
       
    42 
       
    43 
       
    44 ## run it!
       
    45 
       
    46 START_SML="$INFILE $ML_OPTIONS"
       
    47 
       
    48 if [ -n "$TERMINATE" ]; then
       
    49   { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
       
    50   RC=$?
       
    51 else
       
    52   { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat; echo "$MLEXIT" } | $START_SML
       
    53   RC=$?
       
    54 fi
       
    55 
       
    56 if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
       
    57   mv -f "$OUTFILE" "$INFILE" || fail_out
       
    58 fi
       
    59 
       
    60 exit $RC