# HG changeset patch
# User wenzelm
# Date 1619127622 -7200
# Node ID 37243ad3ecb61c2de264dd17e5733000fcb0cd99
# Parent  19c558ea903c9466e358b3f85ae086069fcbf3d1
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);

diff -r 19c558ea903c -r 37243ad3ecb6 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Thu Apr 22 23:03:58 2021 +0200
+++ b/src/Pure/System/bash.scala	Thu Apr 22 23:40:22 2021 +0200
@@ -11,6 +11,7 @@
   BufferedWriter, OutputStreamWriter}
 
 import scala.annotation.tailrec
+import scala.jdk.OptionConverters._
 
 
 object Bash
@@ -91,12 +92,18 @@
 
     private val group_pid = stdout.readLine
 
+    private val initial_process: Option[ProcessHandle] =
+      if (Platform.is_unix) ProcessHandle.of(Value.Long.parse(group_pid)).toScala
+      else None
+
     @tailrec private def signal(s: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
         Isabelle_System.process_signal(group_pid, signal = s)
-        val running = Isabelle_System.process_signal(group_pid)
+        val running =
+          (initial_process.isDefined && initial_process.get.isAlive) ||
+          Isabelle_System.process_signal(group_pid)
         if (running) {
           Time.seconds(0.1).sleep
           signal(s, count - 1)
diff -r 19c558ea903c -r 37243ad3ecb6 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Thu Apr 22 23:03:58 2021 +0200
+++ b/src/Pure/System/platform.scala	Thu Apr 22 23:40:22 2021 +0200
@@ -14,6 +14,7 @@
   val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
   val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
   val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
+  val is_unix: Boolean = is_linux || is_macos
 
   def family: Family.Value =
     if (is_linux) Family.linux