src/Pure/PIDE/xml.scala
2012-03-08 wenzelm 2012-03-08 simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
2011-11-29 wenzelm 2011-11-29 separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-28 wenzelm 2011-11-28 explicit indication of modules for independent Scala library;
2011-09-07 wenzelm 2011-09-07 XML.cache for partial sharing (strings only);
2011-09-05 wenzelm 2011-09-05 tuned imports;
2011-09-04 wenzelm 2011-09-04 simplified signatures;
2011-09-04 wenzelm 2011-09-04 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
2011-09-04 wenzelm 2011-09-04 moved XML/YXML to src/Pure/PIDE; tuned comments;