--- 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 }