# HG changeset patch
# User wenzelm
# Date 1753616945 -7200
# Node ID 51c57bbb27f722d9ffc2db2be55f2976938af35a
# Parent  99a720d3ed8fe962474bf14832588c99593183f4
clarified signature;

diff -r 99a720d3ed8f -r 51c57bbb27f7 src/Pure/Build/build.scala
--- 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)
diff -r 99a720d3ed8f -r 51c57bbb27f7 src/Pure/PIDE/rendering.scala
--- 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 =>