| 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 =>