--- 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))
--- 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 =