src/Pure/PIDE/protocol.scala

--- a/src/Pure/PIDE/protocol.scala	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Mar 21 18:37:05 2025 +0100
@@ -107,6 +107,12 @@
 
   /* result messages */
 
+  def is_urgent(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(_, props), _) => Markup.Urgent.get(props)
+      case _ => false
+    }
+
   def is_result(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.RESULT, _), _) => true