more robust: prefer tail-recursive traversal;

--- a/src/Pure/PIDE/xml.scala	Thu Jun 27 23:36:19 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Jun 27 23:45:32 2024 +0200
@@ -124,13 +124,14 @@
   /* traverse text */
 
   def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = {
-    def traverse(x: A, t: Tree): A =
-      t match {
-        case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
-        case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
-        case XML.Text(s) => op(x, s)
+    @tailrec def trav(x: A, list: List[Tree]): A =
+      list match {
+        case Nil => x
+        case XML.Wrapped_Elem(_, _, body) :: rest => trav(x, body ::: rest)
+        case XML.Elem(_, body) :: rest => trav(x, body ::: rest)
+        case XML.Text(s) :: rest => trav(op(x, s), rest)
       }
-    body.foldLeft(a)(traverse)
+    trav(a, body)
   }
 
   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }