tuned comments;
authorwenzelm
Fri, 06 Jan 2023 15:35:48 +0100
changeset 76932 f88c239d1a83
parent 76931 cca0b48ca891
child 76933 dd53bb198eb1
tuned comments;
src/Pure/PIDE/document.scala
--- 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) <-