clarified signature;
authorwenzelm
Sun, 27 Jul 2025 13:49:05 +0200
changeset 82903 51c57bbb27f7
parent 82902 99a720d3ed8f
child 82904 82a8176f89dd
clarified signature;
src/Pure/Build/build.scala
src/Pure/PIDE/rendering.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)
--- 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 =>