--- a/src/Pure/Build/build.scala Thu Jul 24 17:46:29 2025 +0200
+++ b/src/Pure/Build/build.scala Sun Jul 27 13:49:05 2025 +0200
@@ -820,7 +820,7 @@
case Some(snapshot) =>
val rendering = new Rendering(snapshot, options, session)
val messages =
- rendering.text_messages(Text.Range.full)
+ rendering.text_messages()
.filter(message => progress.verbose || Protocol.is_exported(message.info))
if (messages.nonEmpty) {
val line_document = Line.Document(snapshot.node.source)
--- a/src/Pure/PIDE/rendering.scala Thu Jul 24 17:46:29 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala Sun Jul 27 13:49:05 2025 +0200
@@ -570,7 +570,7 @@
} yield Text.Info(r, color)
}
- def text_messages(range: Text.Range): List[Text.Info[XML.Elem]] = {
+ def text_messages(range: Text.Range = Text.Range.full): List[Text.Info[XML.Elem]] = {
val results =
snapshot.cumulate[Vector[Command.Results.Entry]](
range, Vector.empty, Rendering.message_elements, command_states =>