author | wenzelm |
Fri, 06 Jan 2023 15:35:48 +0100 | |
changeset 76932 | f88c239d1a83 |
parent 76931 | cca0b48ca891 |
child 76933 | dd53bb198eb1 |
--- a/src/Pure/PIDE/document.scala Fri Jan 06 14:59:59 2023 +0100 +++ b/src/Pure/PIDE/document.scala Fri Jan 06 15:35:48 2023 +0100 @@ -643,16 +643,13 @@ } - /* XML markup */ + /* markup and messages */ def xml_markup( range: Text.Range = Text.Range.full, elements: Markup.Elements = Markup.Elements.full): XML.Body = state.xml_markup(version, node_name, range = range, elements = elements) - - /* messages */ - lazy val messages: List[(XML.Elem, Position.T)] = (for { (command, start) <-