# HG changeset patch
# User wenzelm
# Date 1586199873 -7200
# Node ID c6b7f4da67b3f27601dfd69cfa62c6328a51261f
# Parent  d9aaafcd872b1e5678e05540537647dc31f41064
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);

diff -r d9aaafcd872b -r c6b7f4da67b3 src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 20:11:07 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 21:04:33 2020 +0200
@@ -20,6 +20,9 @@
       case _ => error("Isabelle-specific thread required")
     }
 
+  def check_self: Boolean =
+    Thread.currentThread.isInstanceOf[Isabelle_Thread]
+
 
   /* create threads */
 
@@ -107,6 +110,10 @@
 
   def uninterruptible[A](body: => A): A =
     interrupt_handler(Interrupt_Handler.uninterruptible)(body)
+
+  def try_uninterruptible[A](body: => A): A =
+    if (check_self) interrupt_handler(Interrupt_Handler.uninterruptible)(body)
+    else body
 }
 
 class Isabelle_Thread private(main: Runnable, name: String, group: ThreadGroup,
diff -r d9aaafcd872b -r c6b7f4da67b3 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Mon Apr 06 20:11:07 2020 +0200
+++ b/src/Pure/System/bash.scala	Mon Apr 06 21:04:33 2020 +0200
@@ -116,14 +116,14 @@
       }
     }
 
-    def terminate(): Unit = Isabelle_Thread.uninterruptible
+    def terminate(): Unit = Isabelle_Thread.try_uninterruptible
     {
       kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
       proc.destroy
       do_cleanup()
     }
 
-    def interrupt(): Unit = Isabelle_Thread.uninterruptible
+    def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
     {
       Isabelle_System.kill("INT", pid)
     }
@@ -131,7 +131,7 @@
 
     // JVM shutdown hook
 
-    private val shutdown_hook = new Thread { override def run = terminate() }
+    private val shutdown_hook = Isabelle_Thread.create(() => terminate())
 
     try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
     catch { case _: IllegalStateException => }