minor performance tuning;
authorwenzelm
Sat, 29 Jun 2024 14:57:04 +0200
changeset 80457 b2c4ba0d048b
parent 80456 bd95c65f241e
child 80458 b66ece8770a9
minor performance tuning;
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 =>