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