tuned;

--- a/src/Pure/PIDE/xml.scala	Fri Jun 28 00:15:34 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Jun 28 00:26:02 2024 +0200
@@ -137,9 +137,6 @@
   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
   def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
 
-
-  /* text content */
-
   def content(body: Body): String = {
     val text = new StringBuilder(text_length(body))
     traverse_text(body)(()) { case (_, s) => text.append(s) }