src/Pure/PIDE/xml.ML
Sat, 02 Nov 2019 13:25:58 +0100 wenzelm unused;
Sat, 02 Nov 2019 12:33:38 +0100 wenzelm clarified signature;
Sat, 02 Nov 2019 12:02:27 +0100 wenzelm more scalable protocol_message: use XML.body directly (Output.output hook is not required);
Thu, 10 Oct 2019 16:51:47 +0200 wenzelm more compact XML representation;
Thu, 14 Feb 2019 15:45:34 +0100 wenzelm tuned according to Scala version;
Thu, 14 Feb 2019 14:44:41 +0100 wenzelm uniform XML header;
Thu, 03 Jan 2019 12:34:26 +0100 wenzelm tuned;
Sun, 25 Nov 2018 21:10:55 +0100 wenzelm tuned signature (see also src/Tools/Haskell/Markup.hs);
Sun, 04 Nov 2018 17:19:56 +0100 wenzelm more Haskell operations;
Sat, 03 Nov 2018 19:31:50 +0100 wenzelm tuned comments;
Mon, 20 Mar 2017 15:37:14 +0100 wenzelm more operations;
Mon, 05 Sep 2016 23:11:00 +0200 wenzelm clarified modules;
Sat, 02 Apr 2016 21:10:07 +0200 wenzelm careful export of type-dependent functions, without losing their special status;
Fri, 18 Mar 2016 16:26:35 +0100 wenzelm clarified modules;
Thu, 19 Nov 2015 22:35:10 +0100 wenzelm tuned;
Sun, 18 Oct 2015 21:30:01 +0200 wenzelm tuned signature;
Thu, 20 Aug 2015 13:41:53 +0200 wenzelm precise BinIO, without newline conversion on Windows;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
Wed, 12 Mar 2014 14:17:13 +0100 wenzelm some document antiquotations for Isabelle/jEdit elements;
Fri, 28 Sep 2012 22:53:18 +0200 wenzelm support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
Wed, 26 Sep 2012 19:50:10 +0200 wenzelm discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
Sat, 11 Aug 2012 17:40:33 +0200 wenzelm tuned message;
Thu, 29 Mar 2012 22:43:50 +0200 wenzelm more specific notion of partiality (cf. Scala version);
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