src/Pure/PIDE/rendering.scala
changeset 82903 51c57bbb27f7
parent 82796 ad3860303ebb
child 82926 f4bc5313c821
--- 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 =>