--- a/src/Pure/PIDE/session.scala Sun May 13 16:33:11 2018 +0200
+++ b/src/Pure/PIDE/session.scala Sun May 13 16:37:36 2018 +0200
@@ -118,7 +118,7 @@
{
session =>
- val xml_cache: XML.Cache = new XML.Cache()
+ val xml_cache: XML.Cache = XML.make_cache()
val xz_cache: XZ.Cache = XZ.make_cache()