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,