# HG changeset patch
# User wenzelm
# Date 1439847912 -7200
# Node ID faa452d8e265c59dc033a703c787d15777679d71
# Parent  49d1ea25f1a4bbd935eed543b3d5a6e10f58c09f
basic setup for native Windows (RAW session without image);

diff -r 49d1ea25f1a4 -r faa452d8e265 lib/scripts/run-polyml-5.5.3
--- a/lib/scripts/run-polyml-5.5.3	Mon Aug 17 23:16:03 2015 +0200
+++ b/lib/scripts/run-polyml-5.5.3	Mon Aug 17 23:45:12 2015 +0200
@@ -42,10 +42,17 @@
 
 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 _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
   EXIT=""
 fi
 
@@ -53,7 +60,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 \"$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
diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/Concurrent/bash_windows.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash_windows.ML	Mon Aug 17 23:45:12 2015 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Pure/Concurrent/bash.ML
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts -- on native Windows (MinGW).
+*)
+
+signature BASH =
+sig
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+fun process _ = raise Fail "FIXME";
+
+end;
diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/ML-Systems/ml_system.ML
--- a/src/Pure/ML-Systems/ml_system.ML	Mon Aug 17 23:16:03 2015 +0200
+++ b/src/Pure/ML-Systems/ml_system.ML	Mon Aug 17 23:45:12 2015 +0200
@@ -11,6 +11,7 @@
   val is_smlnj: bool
   val platform: string
   val platform_is_cygwin: bool
+  val platform_is_windows: bool
   val share_common_data: unit -> unit
   val save_state: string -> unit
 end;
@@ -24,6 +25,7 @@
 
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_cygwin = String.isSuffix "cygwin" platform;
+val platform_is_windows = String.isSuffix "windows" platform;
 
 fun share_common_data () = ();
 fun save_state _ = raise Fail "Cannot save state -- undefined operation";
diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 23:16:03 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 23:45:12 2015 +0200
@@ -31,6 +31,8 @@
 then use "ML-Systems/share_common_data_polyml-5.3.0.ML"
 else ();
 
+if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else ();
+
 structure ML_System =
 struct
 
diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/ML-Systems/windows_polyml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/windows_polyml.ML	Mon Aug 17 23:45:12 2015 +0200
@@ -0,0 +1,5 @@
+(*  Title:      Pure/ML-Systems/windows_polyml.ML
+    Author:     Makarius
+
+Poly/ML support for native Windows (MinGW).
+*)
diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Aug 17 23:16:03 2015 +0200
+++ b/src/Pure/ROOT	Mon Aug 17 23:45:12 2015 +0200
@@ -34,6 +34,7 @@
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
+    "ML-Systems/windows_polyml.ML"
 
 session Pure =
   global_theories Pure
@@ -69,9 +70,11 @@
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
+    "ML-Systems/windows_polyml.ML"
 
     "Concurrent/bash.ML"
     "Concurrent/bash_sequential.ML"
+    "Concurrent/bash_windows.ML"
     "Concurrent/cache.ML"
     "Concurrent/counter.ML"
     "Concurrent/event_timer.ML"
diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 17 23:16:03 2015 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 17 23:45:12 2015 +0200
@@ -115,9 +115,9 @@
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
-if Multithreading.available
-then use "Concurrent/bash.ML"
-else use "Concurrent/bash_sequential.ML";
+if not Multithreading.available then use "Concurrent/bash_sequential.ML"
+else if ML_System.platform_is_windows then use "Concurrent/bash_windows.ML"
+else use "Concurrent/bash.ML";
 
 use "Concurrent/par_exn.ML";
 use "Concurrent/task_queue.ML";
diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/build
--- a/src/Pure/build	Mon Aug 17 23:16:03 2015 +0200
+++ b/src/Pure/build	Mon Aug 17 23:45:12 2015 +0200
@@ -61,11 +61,11 @@
 if [ "$TARGET" = RAW ]; then
   if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
-      -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \
+      -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
   else
     "$ISABELLE_PROCESS" \
-      -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \
+      -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -e "structure Isar = struct fun main () = () end;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
       -q -w RAW_ML_SYSTEM "$OUTPUT"
@@ -73,11 +73,11 @@
 else
   if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
-      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
+      -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
   else
     "$ISABELLE_PROCESS" \
-      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \
+      -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
       -e "Command_Line.tool0 Session.finish;" \
       -e "Options.reset_default ();" \