# HG changeset patch
# User wenzelm
# Date 1673015748 -3600
# Node ID f88c239d1a838959d29bd235549b3b3fa3b4de4f
# Parent  cca0b48ca8916d1f8d5949fce2be41d939f73d8a
tuned comments;

diff -r cca0b48ca891 -r f88c239d1a83 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) <-