lib/scripts/run-polyml

--- a/lib/scripts/run-polyml	Sun Feb 28 19:56:57 2016 +0100
+++ b/lib/scripts/run-polyml	Sun Feb 28 21:20:51 2016 +0100
@@ -1,8 +1,9 @@
 #!/usr/bin/env bash
+# :mode=shellscript:
 #
 # Author: Makarius
 #
-# Startup script for Poly/ML 5.1 ... 5.5.
+# Startup script for Poly/ML 5.6.
 
 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
 
@@ -39,12 +40,30 @@
 
 ## prepare databases
 
+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=""
-  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+  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));"
+      ;;
+    *)
+      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+      ;;
+  esac
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+  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
 
@@ -52,7 +71,7 @@
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+    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
@@ -64,16 +83,22 @@
 
 MLTEXT="$INIT $EXIT $MLTEXT"
 
-if [ -z "$TERMINATE" ]; then
-  FEEDER_OPTS=""
+if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
+  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+    --error-exit </dev/null
+  RC="$?"
 else
-  FEEDER_OPTS="-q"
+  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"; }
+  RC="$?"
 fi
 
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit "$RC"