--- a/src/Pure/General/html.scala Fri Jun 28 00:26:02 2024 +0200
+++ b/src/Pure/General/html.scala Fri Jun 28 00:30:49 2024 +0200
@@ -244,7 +244,7 @@
case XML.Elem(markup, Nil) =>
xml_output.elem(markup, end = true)
case XML.Elem(Markup(Markup.RAW_HTML, _), body) =>
- XML.traverse_text(body)(()) { case (_, raw) => s.append(raw) }
+ XML.traverse_text(body, (), (_, raw) => s.append(raw))
case XML.Elem(markup, ts) =>
if (structural && structural_elements(markup.name)) s += '\n'
xml_output.elem(markup)
--- a/src/Pure/PIDE/xml.scala Fri Jun 28 00:26:02 2024 +0200
+++ b/src/Pure/PIDE/xml.scala Fri Jun 28 00:30:49 2024 +0200
@@ -123,7 +123,7 @@
/* traverse text */
- def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = {
+ def traverse_text[A](body: Body, a: A, op: (A, String) => A): A = {
@tailrec def trav(x: A, list: List[Tree]): A =
list match {
case Nil => x
@@ -134,12 +134,12 @@
trav(a, body)
}
- def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
- def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
+ 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(body: Body): String = {
val text = new StringBuilder(text_length(body))
- traverse_text(body)(()) { case (_, s) => text.append(s) }
+ traverse_text(body, (), (_, s) => text.append(s))
text.toString
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri Jun 28 00:26:02 2024 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Jun 28 00:30:49 2024 +0200
@@ -251,7 +251,7 @@
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)(
+ XML.traverse_text(formatted, if (XML.text_length(formatted) == 0) 0 else 1,
(n: Int, s: String) => n + Library.count_newlines(s))
val h = painter.getLineHeight * lines + geometry.deco_height