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
   }