tuned signature;

--- a/src/Pure/PIDE/command.scala	Tue Sep 16 12:06:07 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 16 12:14:37 2025 +0200
@@ -57,7 +57,7 @@
     def get(serial: Long): Option[XML.Elem] = rep.get(serial)
     def iterator: Iterator[Results.Entry] = rep.iterator
 
-    lazy val warned: Boolean = rep.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))
+    lazy val warned: Boolean = rep.exists(p => Protocol.is_warning_or_legacy(p._2))
     lazy val failed: Boolean = rep.exists(p => Protocol.is_error(p._2))
 
     def + (entry: Results.Entry): Results =

--- 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