--- a/src/Pure/Concurrent/bash.scala Tue Aug 25 16:49:14 2015 +0200
+++ b/src/Pure/Concurrent/bash.scala Wed Aug 26 13:43:24 2015 +0200
@@ -60,12 +60,10 @@
private val pid = stdout.readLine
- private def kill_cmd(signal: String): Int =
- Isabelle_System.execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid)
- .waitFor
-
private def kill(signal: String): Boolean =
- Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
+ Exn.Interrupt.postpone {
+ Isabelle_System.kill(signal, pid)
+ Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
private def multi_kill(signal: String): Boolean =
{
--- a/src/Pure/System/isabelle_system.scala Tue Aug 25 16:49:14 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Aug 26 13:43:24 2015 +0200
@@ -290,6 +290,18 @@
}
+ /* kill */
+
+ def kill(signal: String, group_pid: String): (String, Int) =
+ {
+ val bash =
+ if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\bash.exe")
+ else List("/usr/bin/env", "bash")
+ val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
+ process_output(raw_execute(null, null, true, cmdline: _*))
+ }
+
+
/* bash */
private class Limited_Progress(proc: Bash.Process, progress_limit: Option[Long])