# HG changeset patch
# User wenzelm
# Date 1619125438 -7200
# Node ID 19c558ea903c9466e358b3f85ae086069fcbf3d1
# Parent  32839247930844ed8d4ecc3fac87a924b8b38ef8
clarified signature;

diff -r 328392479308 -r 19c558ea903c src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Thu Apr 22 22:55:41 2021 +0200
+++ b/src/Pure/System/bash.scala	Thu Apr 22 23:03:58 2021 +0200
@@ -89,17 +89,17 @@
 
     // signals
 
-    private val pid = stdout.readLine
+    private val group_pid = stdout.readLine
 
-    @tailrec private def kill(signal: String, count: Int = 1): Boolean =
+    @tailrec private def signal(s: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
-        Isabelle_System.kill(signal, pid)
-        val running = Isabelle_System.kill("0", pid)._2 == 0
+        Isabelle_System.process_signal(group_pid, signal = s)
+        val running = Isabelle_System.process_signal(group_pid)
         if (running) {
           Time.seconds(0.1).sleep
-          kill(signal, count - 1)
+          signal(s, count - 1)
         }
         else false
       }
@@ -107,14 +107,14 @@
 
     def terminate(): Unit = Isabelle_Thread.try_uninterruptible
     {
-      kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
+      signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL")
       proc.destroy()
       do_cleanup()
     }
 
     def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
     {
-      Isabelle_System.kill("INT", pid)
+      Isabelle_System.process_signal(group_pid, "INT")
     }
 
 
diff -r 328392479308 -r 19c558ea903c src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Apr 22 22:55:41 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Apr 22 23:03:58 2021 +0200
@@ -496,12 +496,13 @@
     (output, rc)
   }
 
-  def kill(signal: String, group_pid: String): (String, Int) =
+  def process_signal(group_pid: String, signal: String = "0"): Boolean =
   {
     val bash =
       if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
       else List("/usr/bin/env", "bash")
-    process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
+    val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
+    rc == 0
   }