src/Pure/PIDE/xml.scala

   }
 
   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) }
     text.toString
   }