diff -r bd95c65f241e -r b2c4ba0d048b src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Sat Jun 29 14:48:20 2024 +0200 +++ b/src/Pure/PIDE/xml.scala Sat Jun 29 14:57:04 2024 +0200 @@ -155,9 +155,13 @@ 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_is_empty(body: Body): Boolean = + traverse_text(body, true, (b, s) => b && s.isEmpty) + + def content_lines(body: Body): Int = { + val n = traverse_text(body, 0, (n, s) => n + Library.count_newlines(s)) + if (n == 0 && content_is_empty(body)) 0 else n + 1 + } def content(body: Body): String = Library.string_builder(hint = text_length(body)) { text =>