clarified files;
authorwenzelm
Thu, 10 Mar 2016 09:50:53 +0100
changeset 62584 6cd36a0d2a28
parent 62579 bfa38c2e751f
child 62585 5d4ed917450d
clarified files;
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash.scala
src/Pure/Concurrent/bash_windows.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/bash.ML
src/Pure/System/bash.scala
src/Pure/System/bash_windows.ML
src/Pure/build-jars
--- a/src/Pure/Concurrent/bash.ML	Wed Mar 09 21:01:22 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(*  Title:      Pure/Concurrent/bash.ML
-    Author:     Makarius
-
-GNU bash processes, with propagation of interrupts -- POSIX version.
-*)
-
-signature BASH =
-sig
-  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
-end;
-
-structure Bash: BASH =
-struct
-
-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 =
-      Standard_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 _ = getenv_strict "ISABELLE_BASH_PROCESS";
-            val status =
-              OS.Process.system
-                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
-                  " bash " ^ File.bash_path script_path ^
-                  " > " ^ File.bash_path out_path ^
-                  " 2> " ^ File.bash_path err_path);
-            val res =
-              (case Posix.Process.fromStatus status of
-                Posix.Process.W_EXITED => Result 0
-              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
-              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
-              | Posix.Process.W_SIGNALED s =>
-                  if s = Posix.Signal.int then Signal
-                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
-              | Posix.Process.W_STOPPED s =>
-                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
-          in Synchronized.change result (K res) end
-          handle exn =>
-            (Synchronized.change result (fn Wait => Signal | res => res); Exn.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 =
-              (Posix.Process.kill
-                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
-              handle OS.SysErr _ => false;
-
-            fun multi_kill count s =
-              count = 0 orelse
-                (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
-                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
-            val _ =
-              multi_kill 10 Posix.Signal.int andalso
-              multi_kill 10 Posix.Signal.term andalso
-              multi_kill 10 Posix.Signal.kill;
-          in () end;
-
-    fun cleanup () =
-     (Standard_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 (); Exn.reraise exn)
-  end);
-
-end;
-
--- a/src/Pure/Concurrent/bash.scala	Wed Mar 09 21:01:22 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,168 +0,0 @@
-/*  Title:      Pure/Concurrent/bash.scala
-    Author:     Makarius
-
-GNU bash processes, with propagation of interrupts.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile, BufferedReader, InputStreamReader,
-  BufferedWriter, OutputStreamWriter}
-
-
-object Bash
-{
-  private class Limited_Progress(proc: Process, progress_limit: Option[Long])
-  {
-    private var count = 0L
-    def apply(progress: String => Unit)(line: String): Unit = synchronized {
-      progress(line)
-      count = count + line.length + 1
-      progress_limit match {
-        case Some(limit) if count > limit => proc.terminate
-        case _ =>
-      }
-    }
-  }
-
-  def process(script: String,
-      cwd: JFile = null,
-      env: Map[String, String] = Map.empty,
-      redirect: Boolean = false): Process =
-    new Process(script, cwd, env, redirect)
-
-  class Process private [Bash](
-      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
-    extends Prover.System_Process
-  {
-    private val timing_file = Isabelle_System.tmp_file("bash_script")
-    private val timing = Synchronized[Option[Timing]](None)
-
-    private val script_file = Isabelle_System.tmp_file("bash_script")
-    File.write(script_file, script)
-
-    private val proc =
-      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
-        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
-          File.standard_path(timing_file), "bash", File.standard_path(script_file))
-
-
-    // channels
-
-    val stdin: BufferedWriter =
-      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
-
-    val stdout: BufferedReader =
-      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
-
-    val stderr: BufferedReader =
-      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
-
-
-    // signals
-
-    private val pid = stdout.readLine
-
-    def interrupt()
-    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
-
-    private def kill(signal: String): Boolean =
-      Exn.Interrupt.postpone {
-        Isabelle_System.kill(signal, pid)
-        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
-
-    private def multi_kill(signal: String): Boolean =
-    {
-      var running = true
-      var count = 10
-      while (running && count > 0) {
-        if (kill(signal)) {
-          Exn.Interrupt.postpone {
-            Thread.sleep(100)
-            count -= 1
-          }
-        }
-        else running = false
-      }
-      running
-    }
-
-    def terminate()
-    {
-      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
-      proc.destroy
-      cleanup()
-    }
-
-
-    // JVM shutdown hook
-
-    private val shutdown_hook = new Thread { override def run = terminate() }
-
-    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
-    catch { case _: IllegalStateException => }
-
-
-    // cleanup
-
-    private def cleanup()
-    {
-      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
-      catch { case _: IllegalStateException => }
-
-      script_file.delete
-
-      timing.change {
-        case None =>
-          if (timing_file.isFile) {
-            val t =
-              Word.explode(File.read(timing_file)) match {
-                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
-                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
-                case _ => Timing.zero
-              }
-            timing_file.delete
-            Some(t)
-          }
-          else Some(Timing.zero)
-        case some => some
-      }
-    }
-
-
-    // join
-
-    def join: Int =
-    {
-      val rc = proc.waitFor
-      cleanup()
-      rc
-    }
-
-
-    // result
-
-    def result(
-      progress_stdout: String => Unit = (_: String) => (),
-      progress_stderr: String => Unit = (_: String) => (),
-      progress_limit: Option[Long] = None,
-      strict: Boolean = true): Process_Result =
-    {
-      stdin.close
-
-      val limited = new Limited_Progress(this, progress_limit)
-      val out_lines =
-        Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
-      val err_lines =
-        Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
-
-      val rc =
-        try { join }
-        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
-      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
-
-      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
-    }
-  }
-}
--- a/src/Pure/Concurrent/bash_windows.ML	Wed Mar 09 21:01:22 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(*  Title:      Pure/Concurrent/bash_windows.ML
-    Author:     Makarius
-
-GNU bash processes, with propagation of interrupts -- Windows version.
-*)
-
-signature BASH =
-sig
-  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
-end;
-
-structure Bash: BASH =
-struct
-
-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 =
-      Standard_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 bash_script =
-              "bash " ^ File.bash_path script_path ^
-                " > " ^ File.bash_path out_path ^
-                " 2> " ^ File.bash_path err_path;
-            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
-            val rc =
-              Windows.simpleExecute ("",
-                quote (ML_System.platform_path bash_process) ^ " " ^
-                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
-              |> 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); Exn.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 =
-              let
-                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
-                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
-              in
-                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
-                  handle OS.SysErr _ => false
-              end;
-
-            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 () =
-     (Standard_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 (); Exn.reraise exn)
-  end);
-
-end;
--- a/src/Pure/ROOT	Wed Mar 09 21:01:22 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 10 09:50:53 2016 +0100
@@ -3,8 +3,6 @@
 session Pure =
   global_theories Pure
   files
-    "Concurrent/bash.ML"
-    "Concurrent/bash_windows.ML"
     "Concurrent/cache.ML"
     "Concurrent/counter.ML"
     "Concurrent/event_timer.ML"
@@ -153,6 +151,8 @@
     "Syntax/syntax_trans.ML"
     "Syntax/term_position.ML"
     "Syntax/type_annotation.ML"
+    "System/bash.ML"
+    "System/bash_windows.ML"
     "System/command_line.ML"
     "System/invoke_scala.ML"
     "System/isabelle_process.ML"
--- a/src/Pure/ROOT.ML	Wed Mar 09 21:01:22 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 10 09:50:53 2016 +0100
@@ -193,10 +193,6 @@
 use "Concurrent/standard_thread.ML";
 use "Concurrent/single_assignment.ML";
 
-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";
 use "Concurrent/future.ML";
@@ -371,8 +367,13 @@
 use "Proof/proof_checker.ML";
 use "Proof/extraction.ML";
 
+(*Isabelle system*)
+if ML_System.platform_is_windows
+then use "System/bash_windows.ML"
+else use "System/bash.ML";
+use "System/isabelle_system.ML";
+
 (*theory documents*)
-use "System/isabelle_system.ML";
 use "Thy/term_style.ML";
 use "Isar/outer_syntax.ML";
 use "Thy/thy_output.ML";
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash.ML	Thu Mar 10 09:50:53 2016 +0100
@@ -0,0 +1,102 @@
+(*  Title:      Pure/System/bash.ML
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts -- POSIX version.
+*)
+
+signature BASH =
+sig
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+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 =
+      Standard_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 _ = getenv_strict "ISABELLE_BASH_PROCESS";
+            val status =
+              OS.Process.system
+                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
+                  " bash " ^ File.bash_path script_path ^
+                  " > " ^ File.bash_path out_path ^
+                  " 2> " ^ File.bash_path err_path);
+            val res =
+              (case Posix.Process.fromStatus status of
+                Posix.Process.W_EXITED => Result 0
+              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
+              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
+              | Posix.Process.W_SIGNALED s =>
+                  if s = Posix.Signal.int then Signal
+                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
+              | Posix.Process.W_STOPPED s =>
+                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
+          in Synchronized.change result (K res) end
+          handle exn =>
+            (Synchronized.change result (fn Wait => Signal | res => res); Exn.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 =
+              (Posix.Process.kill
+                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
+              handle OS.SysErr _ => false;
+
+            fun multi_kill count s =
+              count = 0 orelse
+                (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
+                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+            val _ =
+              multi_kill 10 Posix.Signal.int andalso
+              multi_kill 10 Posix.Signal.term andalso
+              multi_kill 10 Posix.Signal.kill;
+          in () end;
+
+    fun cleanup () =
+     (Standard_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 (); Exn.reraise exn)
+  end);
+
+end;
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash.scala	Thu Mar 10 09:50:53 2016 +0100
@@ -0,0 +1,168 @@
+/*  Title:      Pure/System/bash.scala
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile, BufferedReader, InputStreamReader,
+  BufferedWriter, OutputStreamWriter}
+
+
+object Bash
+{
+  private class Limited_Progress(proc: Process, progress_limit: Option[Long])
+  {
+    private var count = 0L
+    def apply(progress: String => Unit)(line: String): Unit = synchronized {
+      progress(line)
+      count = count + line.length + 1
+      progress_limit match {
+        case Some(limit) if count > limit => proc.terminate
+        case _ =>
+      }
+    }
+  }
+
+  def process(script: String,
+      cwd: JFile = null,
+      env: Map[String, String] = Map.empty,
+      redirect: Boolean = false): Process =
+    new Process(script, cwd, env, redirect)
+
+  class Process private [Bash](
+      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
+    extends Prover.System_Process
+  {
+    private val timing_file = Isabelle_System.tmp_file("bash_script")
+    private val timing = Synchronized[Option[Timing]](None)
+
+    private val script_file = Isabelle_System.tmp_file("bash_script")
+    File.write(script_file, script)
+
+    private val proc =
+      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
+        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+          File.standard_path(timing_file), "bash", File.standard_path(script_file))
+
+
+    // channels
+
+    val stdin: BufferedWriter =
+      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
+
+    val stdout: BufferedReader =
+      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
+
+    val stderr: BufferedReader =
+      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
+
+
+    // signals
+
+    private val pid = stdout.readLine
+
+    def interrupt()
+    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
+
+    private def kill(signal: String): Boolean =
+      Exn.Interrupt.postpone {
+        Isabelle_System.kill(signal, pid)
+        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
+
+    private def multi_kill(signal: String): Boolean =
+    {
+      var running = true
+      var count = 10
+      while (running && count > 0) {
+        if (kill(signal)) {
+          Exn.Interrupt.postpone {
+            Thread.sleep(100)
+            count -= 1
+          }
+        }
+        else running = false
+      }
+      running
+    }
+
+    def terminate()
+    {
+      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
+      proc.destroy
+      cleanup()
+    }
+
+
+    // JVM shutdown hook
+
+    private val shutdown_hook = new Thread { override def run = terminate() }
+
+    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
+    catch { case _: IllegalStateException => }
+
+
+    // cleanup
+
+    private def cleanup()
+    {
+      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+      catch { case _: IllegalStateException => }
+
+      script_file.delete
+
+      timing.change {
+        case None =>
+          if (timing_file.isFile) {
+            val t =
+              Word.explode(File.read(timing_file)) match {
+                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
+                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
+                case _ => Timing.zero
+              }
+            timing_file.delete
+            Some(t)
+          }
+          else Some(Timing.zero)
+        case some => some
+      }
+    }
+
+
+    // join
+
+    def join: Int =
+    {
+      val rc = proc.waitFor
+      cleanup()
+      rc
+    }
+
+
+    // result
+
+    def result(
+      progress_stdout: String => Unit = (_: String) => (),
+      progress_stderr: String => Unit = (_: String) => (),
+      progress_limit: Option[Long] = None,
+      strict: Boolean = true): Process_Result =
+    {
+      stdin.close
+
+      val limited = new Limited_Progress(this, progress_limit)
+      val out_lines =
+        Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
+      val err_lines =
+        Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
+
+      val rc =
+        try { join }
+        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
+      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+
+      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
+    }
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash_windows.ML	Thu Mar 10 09:50:53 2016 +0100
@@ -0,0 +1,99 @@
+(*  Title:      Pure/Concurrent/bash_windows.ML
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts -- Windows version.
+*)
+
+signature BASH =
+sig
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
+struct
+
+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 =
+      Standard_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 bash_script =
+              "bash " ^ File.bash_path script_path ^
+                " > " ^ File.bash_path out_path ^
+                " 2> " ^ File.bash_path err_path;
+            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
+            val rc =
+              Windows.simpleExecute ("",
+                quote (ML_System.platform_path bash_process) ^ " " ^
+                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
+              |> 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); Exn.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 =
+              let
+                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
+                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
+              in
+                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
+                  handle OS.SysErr _ => false
+              end;
+
+            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 () =
+     (Standard_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 (); Exn.reraise exn)
+  end);
+
+end;
--- a/src/Pure/build-jars	Wed Mar 09 21:01:22 2016 +0100
+++ b/src/Pure/build-jars	Thu Mar 10 09:50:53 2016 +0100
@@ -9,7 +9,6 @@
 ## sources
 
 declare -a SOURCES=(
-  Concurrent/bash.scala
   Concurrent/consumer_thread.scala
   Concurrent/counter.scala
   Concurrent/event_timer.scala
@@ -74,6 +73,7 @@
   PIDE/xml.scala
   PIDE/yxml.scala
   ROOT.scala
+  System/bash.scala
   System/command_line.scala
   System/cygwin.scala
   System/getopts.scala