src/Pure/PIDE/xml.scala
2017-01-07 ago Line.Document consists of independently allocated strings;
2016-10-24 ago discontinued unused / untested distinction of separate PIDE modules;
2016-10-23 ago more operations (see also properties.ML);
2016-10-23 ago tuned;
2015-08-26 ago tuned signature;
2015-05-03 ago misc tuning, based on warnings by IntelliJ IDEA;
2014-08-12 ago tuned;
2014-08-12 ago more compact representation of special string values;
2014-02-20 ago tuned imports;
2013-08-07 ago tuned signature;
2013-05-14 ago tuned signature;
2013-04-09 ago tuned signature;
2013-02-19 ago help JVM to cope with large symbolic structures;
2012-09-28 ago support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-27 ago removed obsolete org.w3c.dom operations;
2012-09-20 ago tuned signature;
2012-09-20 ago tuned;
2012-09-18 ago recover order of stacked markup;
2012-09-18 ago some actual rich text markup via XML.content_markup;
2012-03-08 ago simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
2011-11-29 ago separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-28 ago explicit indication of modules for independent Scala library;
2011-09-07 ago XML.cache for partial sharing (strings only);
2011-09-05 ago tuned imports;
2011-09-04 ago simplified signatures;
2011-09-04 ago synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
2011-09-04 ago moved XML/YXML to src/Pure/PIDE;