# HG changeset patch
# User wenzelm
# Date 1586174388 -7200
# Node ID 2e602e278b77f1f0af7b7a3d25306388f54e94b0
# Parent  e95a4c2c94513bacb12b055343e302ad7032eab4
tuned;

diff -r e95a4c2c9451 -r 2e602e278b77 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Mon Apr 06 13:54:45 2020 +0200
+++ b/src/Pure/System/bash.scala	Mon Apr 06 13:59:48 2020 +0200
@@ -102,19 +102,15 @@
 
     private val pid = stdout.readLine
 
-    private def kill(signal: String): Boolean =
-    {
-      Isabelle_System.kill(signal, pid)
-      Isabelle_System.kill("0", pid)._2 == 0
-    }
-
-    @tailrec private def multi_kill(signal: String, count: Int = 10): Boolean =
+    @tailrec private def kill(signal: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
-        if (kill(signal)) {
+        Isabelle_System.kill(signal, pid)
+        val running = Isabelle_System.kill("0", pid)._2 == 0
+        if (running) {
           Time.seconds(0.1).sleep
-          multi_kill(signal, count - 1)
+          kill(signal, count - 1)
         }
         else false
       }
@@ -122,7 +118,7 @@
 
     def terminate(): Unit = Isabelle_Thread.uninterruptible
     {
-      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
+      kill("INT", count = 10) && kill("TERM", count = 10) && kill("KILL")
       proc.destroy
       do_cleanup()
     }