# HG changeset patch
# User wenzelm
# Date 1719665300 -7200
# Node ID bd95c65f241e65ffa960f43efc7ac142ab5fce53
# Parent  99e276c441215b6502f18fae8e75ac4e04f41294
clarified modules;

diff -r 99e276c44121 -r bd95c65f241e 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))
diff -r 99e276c44121 -r bd95c65f241e src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 12:50:43 2024 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Jun 29 14:48:20 2024 +0200
@@ -250,9 +250,7 @@
           ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
 
       val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
-      val lines =
-        XML.traverse_text(formatted, if (XML.text_length(formatted) == 0) 0 else 1,
-          (n: Int, s: String) => n + Library.count_newlines(s))
+      val lines = XML.content_lines(formatted)
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =