diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/xml.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -217,7 +217,7 @@
       else
         lookup(x) match {
           case Some(y) => y
-          case None => x.map(cache_tree(_))
+          case None => x.map(cache_tree)
         }
     }