src/Pure/Build/build.scala
changeset 82933 343e84d8919a
parent 82932 1337812b6d10
child 82948 e2e43992f339
--- 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]