# HG changeset patch
# User wenzelm
# Date 1719524732 -7200
# Node ID de2ea807edd2fa30198e2f258efe7dc6c514de51
# Parent  6f1c8084f67239ad6b2a3ff8460682b4e44ec512
more robust: prefer tail-recursive traversal;

diff -r 6f1c8084f672 -r de2ea807edd2 src/Pure/PIDE/xml.scala
--- 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 }