src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Sat Jun 29 12:50:43 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Sat Jun 29 14:48:20 2024 +0200
@@ -155,6 +155,10 @@
   def text_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + s.length)
   def symbol_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + Symbol.length(s))
 
+  def content_lines(body: Body): Int =
+    traverse_text(body, if (text_length(body) == 0) 0 else 1,
+      (n: Int, s: String) => n + Library.count_newlines(s))
+
   def content(body: Body): String =
     Library.string_builder(hint = text_length(body)) { text =>
       traverse_text(body, (), (_, s) => text.append(s))