# HG changeset patch
# User wenzelm
# Date 1619377979 -7200
# Node ID 342362c9496c33a6337472a953dca6acf5c09b50
# Parent  37243ad3ecb61c2de264dd17e5733000fcb0cd99
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);

diff -r 37243ad3ecb6 -r 342362c9496c src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Thu Apr 22 23:40:22 2021 +0200
+++ b/src/Pure/System/bash.scala	Sun Apr 25 21:12:59 2021 +0200
@@ -66,8 +66,18 @@
     private val timing = Synchronized[Option[Timing]](None)
     def get_timing: Timing = timing.value getOrElse Timing.zero
 
-    private val script_file = Isabelle_System.tmp_file("bash_script")
-    File.write(script_file, script)
+    private val winpid_file: Option[JFile] =
+      if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None
+    private val winpid_script =
+      winpid_file match {
+        case None => script
+        case Some(file) =>
+          "read < /proc/self/winpid > /dev/null 2> /dev/null\n" +
+          """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script
+      }
+
+    private val script_file: JFile = Isabelle_System.tmp_file("bash_script")
+    File.write(script_file, winpid_script)
 
     private val proc =
       Isabelle_System.process(
@@ -92,18 +102,25 @@
 
     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
+    private def process_alive(pid: String): Boolean =
+      (for {
+        p <- Value.Long.unapply(pid)
+        handle <- ProcessHandle.of(p).toScala
+      } yield handle.isAlive) getOrElse false
+
+    private def root_process_alive(): Boolean =
+      winpid_file match {
+        case None => process_alive(group_pid)
+        case Some(file) =>
+          file.exists() && process_alive(Library.trim_line(File.read(file)))
+      }
 
     @tailrec private def signal(s: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
         Isabelle_System.process_signal(group_pid, signal = s)
-        val running =
-          (initial_process.isDefined && initial_process.get.isAlive) ||
-          Isabelle_System.process_signal(group_pid)
+        val running = root_process_alive() || Isabelle_System.process_signal(group_pid)
         if (running) {
           Time.seconds(0.1).sleep
           signal(s, count - 1)
@@ -140,7 +157,8 @@
       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
       catch { case _: IllegalStateException => }
 
-      script_file.delete
+      script_file.delete()
+      winpid_file.foreach(_.delete())
 
       timing.change {
         case None =>