src/Pure/PIDE/xml.ML
2012-09-28 wenzelm 2012-09-28 support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-26 wenzelm 2012-09-26 discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
2012-08-11 wenzelm 2012-08-11 tuned message;
2012-03-29 wenzelm 2012-03-29 more specific notion of partiality (cf. Scala version);
2012-03-08 wenzelm 2012-03-08 tuned comment;
2012-03-08 wenzelm 2012-03-08 simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
2012-03-08 wenzelm 2012-03-08 clarified XML signature (again) -- coincide with basic Markup without explicit dependency;
2011-10-16 wenzelm 2011-10-16 slightly more standard-conformant XML parsing (see also 94033767ef9b);
2011-09-08 wenzelm 2011-09-08 more substructural sharing to gain significant compression;
2011-09-07 wenzelm 2011-09-07 XML.cache for partial sharing (strings only);
2011-09-04 wenzelm 2011-09-04 moved XML/YXML to src/Pure/PIDE; tuned comments;