src/Pure/PIDE/session.scala
changeset 68169 395432e7516e
parent 68168 a9b49430f061
child 68293 2bc4e5d9cca6
     1.1 --- a/src/Pure/PIDE/session.scala	Sun May 13 16:33:11 2018 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Sun May 13 16:37:36 2018 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  {
     1.5    session =>
     1.6  
     1.7 -  val xml_cache: XML.Cache = new XML.Cache()
     1.8 +  val xml_cache: XML.Cache = XML.make_cache()
     1.9    val xz_cache: XZ.Cache = XZ.make_cache()
    1.10  
    1.11