tuned;
authorwenzelm
Mon, 06 Apr 2020 13:59:48 +0200
changeset 71923 2e602e278b77
parent 71922 e95a4c2c9451
child 71924 dd9fc8a3036c
tuned;
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()
     }