src/Pure/PIDE/xml.ML
Thu, 08 Mar 2012 21:40:15 +0100 wenzelm tuned comment;
Thu, 08 Mar 2012 21:36:36 +0100 wenzelm simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
Thu, 08 Mar 2012 19:56:57 +0100 wenzelm clarified XML signature (again) -- coincide with basic Markup without explicit dependency;
Sun, 16 Oct 2011 16:56:01 +0200 wenzelm slightly more standard-conformant XML parsing (see also 94033767ef9b);
Thu, 08 Sep 2011 00:20:09 +0200 wenzelm more substructural sharing to gain significant compression;
Wed, 07 Sep 2011 23:08:04 +0200 wenzelm XML.cache for partial sharing (strings only);
Sun, 04 Sep 2011 15:21:50 +0200 wenzelm moved XML/YXML to src/Pure/PIDE;
less more (0) tip