diff -r 84b092fd0f7a -r 21a4fd7b04c3 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Sep 16 12:06:07 2025 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Sep 16 12:14:37 2025 +0200
@@ -168,6 +168,9 @@
       case _ => false
     }
 
+  def is_warning_or_legacy(msg: XML.Tree): Boolean =
+    is_warning(msg) || is_legacy(msg)
+
   def is_inlined(msg: XML.Tree): Boolean =
     !(is_result(msg) || is_tracing(msg))
 
@@ -176,7 +179,7 @@
 
   def message_heading(elem: XML.Elem, pos: Position.T): String = {
     val h =
-      if (is_warning(elem) || is_legacy(elem)) "Warning"
+      if (is_warning_or_legacy(elem)) "Warning"
       else if (is_error(elem)) "Error"
       else if (is_information(elem)) "Information"
       else if (is_tracing(elem)) "Tracing"
@@ -200,7 +203,7 @@
         metric = metric, pure = true)
 
     val text2 =
-      if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body)
+      if (is_warning_or_legacy(elem)) Output.warning_prefix(body)
       else if (is_error(elem)) Output.error_message_prefix(body)
       else body