src/Pure/PIDE/xml.ML
2016-09-05 ago clarified modules;
2016-04-02 ago careful export of type-dependent functions, without losing their special status;
2016-03-18 ago clarified modules;
2015-11-19 ago tuned;
2015-10-18 ago tuned signature;
2015-08-20 ago precise BinIO, without newline conversion on Windows;
2014-10-31 ago discontinued obsolete \<^sync> marker;
2014-03-12 ago some document antiquotations for Isabelle/jEdit elements;
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-26 ago discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
2012-08-11 ago tuned message;
2012-03-29 ago more specific notion of partiality (cf. Scala version);
2012-03-08 ago tuned comment;
2012-03-08 ago simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
2012-03-08 ago clarified XML signature (again) -- coincide with basic Markup without explicit dependency;
2011-10-16 ago slightly more standard-conformant XML parsing (see also 94033767ef9b);
2011-09-08 ago more substructural sharing to gain significant compression;
2011-09-07 ago XML.cache for partial sharing (strings only);
2011-09-04 ago moved XML/YXML to src/Pure/PIDE;