clarified signature: builtin filter;

--- a/src/Pure/Build/build.scala	Tue Jul 29 19:59:04 2025 +0200
+++ b/src/Pure/Build/build.scala	Tue Jul 29 22:42:35 2025 +0200
@@ -819,8 +819,8 @@
                 case None => progress.echo(thy_heading + " MISSING")
                 case Some(snapshot) =>
                   val messages =
-                    Rendering.text_messages(snapshot)
-                      .filter(message => progress.verbose || Protocol.is_exported(message.info))
+                    Rendering.text_messages(snapshot,
+                      filter = msg => progress.verbose || Protocol.is_exported(msg))
                   if (messages.nonEmpty) {
                     val line_document = Line.Document(snapshot.node.source)
                     val buffer = new mutable.ListBuffer[String]

--- a/src/Pure/PIDE/rendering.scala	Tue Jul 29 19:59:04 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Jul 29 22:42:35 2025 +0200
@@ -100,15 +100,19 @@
 
   def text_messages(
     snapshot: Document.Snapshot,
-    range: Text.Range = Text.Range.full
+    range: Text.Range = Text.Range.full,
+    filter: XML.Elem => Boolean = _ => true
   ): List[Text.Info[XML.Elem]] = {
     val results =
       snapshot.cumulate[Vector[Command.Results.Entry]](
         range, Vector.empty, message_elements, command_states =>
           {
             case (res, Text.Info(_, elem)) =>
-              Command.State.get_result_proper(command_states, elem.markup.properties)
-                .map(res :+ _)
+              if (filter(elem)) {
+                Command.State.get_result_proper(command_states, elem.markup.properties)
+                  .map(res :+ _)
+              }
+              else None
           })
 
     var seen_serials = Set.empty[Long]