wenzelm@10555: #!/usr/bin/env bash
wenzelm@2302: #
wenzelm@9789: # Author: Markus Wenzel, TU Muenchen
wenzelm@2313: #
wenzelm@5708: # SML/NJ startup script (for 110 or later).
wenzelm@9977: 
wenzelm@10105: export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
wenzelm@2302: 
wenzelm@2302: 
wenzelm@2302: ## diagnostics
wenzelm@2302: 
wenzelm@2349: function fail_out()
wenzelm@2302: {
wenzelm@2349:   echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@2302:   exit 2
wenzelm@2302: }
wenzelm@2302: 
wenzelm@5063: function check_mlhome_file()
wenzelm@5063: {
wenzelm@5063:   if [ ! -f "$1" ]; then
wenzelm@5063:     echo "Unable to locate $1" >&2
wenzelm@5063:     echo "Please check your ML_HOME setting!" >&2
wenzelm@5063:     exit 2
wenzelm@5063:   fi
wenzelm@5063: }
wenzelm@5063: 
wenzelm@6078: function check_heap_file()
wenzelm@6078: {
wenzelm@6078:   if [ ! -f "$1" ]; then
wenzelm@6078:     echo "Expected to find ML heap file $1" >&2
wenzelm@6078:     return 1
wenzelm@6078:   else
wenzelm@6078:     return 0
wenzelm@6078:   fi
wenzelm@6078: }
wenzelm@6078: 
wenzelm@6078: 
wenzelm@5063: 
wenzelm@5063: ## compiler binaries
wenzelm@5063: 
wenzelm@5063: SML="$ML_HOME/sml"
wenzelm@5063: ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
wenzelm@5063: 
wenzelm@5063: check_mlhome_file "$SML"
wenzelm@5063: check_mlhome_file "$ARCH_N_OPSYS"
wenzelm@5063: 
wenzelm@5063: 
wenzelm@2302: 
wenzelm@2302: ## prepare databases
wenzelm@2302: 
wenzelm@4505: if [ -z "$INFILE" ]; then
wenzelm@4505:   EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@4505:   DB=""
wenzelm@4505: else
wenzelm@4505:   EXIT=""
wenzelm@3046:   DB="@SMLload=$INFILE"
wenzelm@2349: fi
wenzelm@2349: 
wenzelm@4505: if [ -z "$OUTFILE" ]; then
wenzelm@4505:   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
wenzelm@4505: else
wenzelm@4505:   COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
wenzelm@4505:   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@4505: fi
wenzelm@2302: 
wenzelm@2302: 
wenzelm@2302: ## run it!
wenzelm@2302: 
wenzelm@4505: MLTEXT="$EXIT $COMMIT $MLTEXT"
wenzelm@4505: MLEXIT="commit();"
wenzelm@2302: 
wenzelm@4505: if [ -z "$TERMINATE" ]; then
wenzelm@4505:   FEEDER_OPTS=""
wenzelm@2302: else
wenzelm@4505:   FEEDER_OPTS="-q"
wenzelm@2302: fi
wenzelm@2302: 
wenzelm@9789: "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@9789:   { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@9789: RC="$?"
wenzelm@3046: 
wenzelm@4505: 
wenzelm@4505: ## fix heap file name and permissions
wenzelm@4505: 
wenzelm@4505: if [ -n "$OUTFILE" ]; then
wenzelm@9789:   eval $("$ARCH_N_OPSYS")
wenzelm@6078:   [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
wenzelm@6078:   HEAP="$OUTFILE.$HEAP_SUFFIX"
wenzelm@6078:   check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
wenzelm@4505:     [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@4505: fi
wenzelm@3503: 
wenzelm@9789: exit "$RC"