lib/scripts/run-polyml

--- a/lib/scripts/run-polyml	Mon Feb 29 16:38:06 2016 +0100
+++ b/lib/scripts/run-polyml	Mon Feb 29 20:35:06 2016 +0100
@@ -5,7 +5,7 @@
 #
 # Startup script for Poly/ML 5.6.
 
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+export -n HEAP_FILE ML_TEXT TERMINATE
 
 
 ## diagnostics
@@ -16,91 +16,55 @@
   exit 2
 }
 
-function fail_out()
-{
-  fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
 function check_file()
 {
   [ ! -f "$1" ] && fail "Unable to locate \"$1\""
 }
 
 
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
+## heap file
 
-case "$ML_PLATFORM" in
-  *-windows)
-    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
-    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
-    ;;
-  *)
-    PLATFORM_INFILE="$INFILE"
-    PLATFORM_OUTFILE="$OUTFILE"
-    ;;
-esac
-
-if [ -z "$INFILE" ]; then
-  INIT=""
+if [ -z "$HEAP_FILE" ]; then
   case "$ML_PLATFORM" in
     *-windows)
-      EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
+      INIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
       ;;
     *)
-      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+      INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
       ;;
   esac
 else
-  check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
-  EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
-  MLEXIT=""
-else
-  if [ -z "$INFILE" ]; then
-    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
-  else
-    MLEXIT="Session.save \"$OUTFILE\";"
-  fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+  check_file "$HEAP_FILE"
+  case "$ML_PLATFORM" in
+    *-windows)
+      PLATFORM_HEAP_FILE="$(platform_path -m "$HEAP_FILE")"
+      ;;
+    *)
+      PLATFORM_HEAP_FILE="$HEAP_FILE"
+      ;;
+  esac
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); OS.Process.exit OS.Process.success));"
 fi
 
 
-## run it!
+## poly process
+
+ML_TEXT="$INIT $ML_TEXT"
 
-MLTEXT="$INIT $EXIT $MLTEXT"
+check_file "$ML_HOME/poly"
+librarypath "$ML_HOME"
 
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
-  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+if [ -n "$TERMINATE" ]; then
+  "$ML_HOME/poly" -q -i $ML_OPTIONS \
+    --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$ML_TEXT")" \
     --error-exit </dev/null
   RC="$?"
 else
-  if [ -z "$TERMINATE" ]; then
-    FEEDER_OPTS=""
-  else
-    FEEDER_OPTS="-q"
-    ML_OPTIONS="$ML_OPTIONS --error-exit"
-  fi
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" | \
+    { read FPID; "$ML_HOME/poly" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
   RC="$?"
 fi
 
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
 exit "$RC"
 
 #:wrap=soft:maxLineLen=100: