src/Pure/PIDE/xml.scala
Wed, 07 Sep 2011 23:08:04 +0200 wenzelm XML.cache for partial sharing (strings only);
less more (0) -1 tip