# HG changeset patch
# User wenzelm
# Date 1440006842 -7200
# Node ID c362c2d0f7251a0e02ce703cd598181a50b6c8d5
# Parent  0a8c719d8c1ffcc07ba9ea5036d31b0e714ad03a
Cygwin bash on Windows;

diff -r 0a8c719d8c1f -r c362c2d0f725 src/Pure/Concurrent/bash_windows.ML
--- a/src/Pure/Concurrent/bash_windows.ML	Wed Aug 19 19:53:45 2015 +0200
+++ b/src/Pure/Concurrent/bash_windows.ML	Wed Aug 19 19:54:02 2015 +0200
@@ -1,7 +1,7 @@
-(*  Title:      Pure/Concurrent/bash.ML
+(*  Title:      Pure/Concurrent/bash_windows.ML
     Author:     Makarius
 
-GNU bash processes, with propagation of interrupts -- on native Windows (MinGW).
+GNU bash processes, with propagation of interrupts -- Windows version.
 *)
 
 signature BASH =
@@ -12,6 +12,83 @@
 structure Bash: BASH =
 struct
 
-fun process _ = raise Fail "FIXME";
+fun cygwin_bash arg =
+  let val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"
+  in Windows.simpleExecute (cmd, quote cmd ^ " -c " ^ quote arg) end;
+
+val process = uninterruptible (fn restore_attributes => fn script =>
+  let
+    datatype result = Wait | Signal | Result of int;
+    val result = Synchronized.var "bash_result" Wait;
+
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+    fun cleanup_files () =
+     (try File.rm script_path;
+      try File.rm out_path;
+      try File.rm err_path;
+      try File.rm pid_path);
+    val _ = cleanup_files ();
+
+    val system_thread =
+      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+          let
+            val _ = File.write script_path script;
+            val rc =
+              cygwin_bash
+                ("echo $$ > " ^ File.shell_path pid_path ^ "; exec bash " ^
+                  File.shell_path script_path ^
+                  " > " ^ File.shell_path out_path ^
+                  " 2> " ^ File.shell_path err_path)
+              |> Windows.fromStatus |> SysWord.toInt;
+            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
+          in Synchronized.change result (K res) end
+          handle exn =>
+            (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
+
+    fun read_pid 0 = NONE
+      | read_pid count =
+          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
+            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
+          | some => some);
+
+    fun terminate NONE = ()
+      | terminate (SOME pid) =
+          let
+            fun kill s =
+              OS.Process.isSuccess (cygwin_bash ("kill -" ^ s ^ " -" ^ string_of_int pid))
+                handle OS.SysErr _ => false;
+            fun multi_kill count s =
+              count = 0 orelse
+                (kill s; kill "0") andalso
+                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+            val _ =
+              multi_kill 10 "INT" andalso
+              multi_kill 10 "TERM" andalso
+              multi_kill 10 "KILL";
+          in () end;
+
+    fun cleanup () =
+     (Simple_Thread.interrupt_unsynchronized system_thread;
+      cleanup_files ());
+  in
+    let
+      val _ =
+        restore_attributes (fn () =>
+          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+      val out = the_default "" (try File.read out_path);
+      val err = the_default "" (try File.read err_path);
+      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+      val pid = read_pid 1;
+      val _ = cleanup ();
+    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
+    handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
+  end);
 
 end;