diff -r 78aa7846e91f -r d8a0e996614b src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -101,11 +101,11 @@
   {
     def traverse(x: A, t: Tree): A =
       t match {
-        case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
-        case XML.Elem(_, ts) => (x /: ts)(traverse)
+        case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
+        case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
         case XML.Text(s) => op(x, s)
       }
-    (a /: body)(traverse)
+    body.foldLeft(a)(traverse)
   }
 
   def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }