--- 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")
}
--- 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
}