src/Pure/PIDE/xml.scala
changeset 81428 257ec066b360
parent 80818 da2557168da7
--- a/src/Pure/PIDE/xml.scala	Mon Nov 11 12:19:45 2024 +0100
+++ b/src/Pure/PIDE/xml.scala	Mon Nov 11 12:47:51 2024 +0100
@@ -177,14 +177,6 @@
   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_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 =>
       traverse_text(body, (), (_, s) => text.append(s))