clarified kill on Windows: just one executable;
authorwenzelm
Wed, 26 Aug 2015 13:43:24 +0200
changeset 61025 636b578bfadd
parent 61024 7b7f01afab71
child 61026 397354b29935
clarified kill on Windows: just one executable;
src/Pure/Concurrent/bash.scala
src/Pure/System/isabelle_system.scala
--- 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])