# HG changeset patch
# User wenzelm
# Date 1719527449 -7200
# Node ID 2990f341e0c6cc5ac75972fc3ae5bd71801641fe
# Parent  73e526bdb0dd17d45df1e21aea9f9fe89f79b93a
tuned signature;

diff -r 73e526bdb0dd -r 2990f341e0c6 src/Pure/General/html.scala
--- 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)
diff -r 73e526bdb0dd -r 2990f341e0c6 src/Pure/PIDE/xml.scala
--- 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
   }
 
diff -r 73e526bdb0dd -r 2990f341e0c6 src/Tools/jEdit/src/pretty_tooltip.scala
--- 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