--- 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
--- /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;
--- 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";
--- 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
--- /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).
+*)
--- 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"
--- 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";
--- 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 ();" \