src/Pure/PIDE/yxml.ML
Sat, 02 Nov 2019 10:56:53 +0100 wenzelm clarified signature;
Sat, 02 Nov 2019 10:43:11 +0100 wenzelm tuned;
Wed, 27 Feb 2019 17:33:39 +0100 wenzelm more scalable on 32-bit Poly/ML;
Sun, 20 May 2018 15:05:45 +0200 wenzelm more scalable;
Mon, 17 Oct 2016 15:46:51 +0200 wenzelm accomodate Poly/ML repository version, which treats singleton strings as boxed;
Sat, 24 Jan 2015 22:00:24 +0100 wenzelm tuned signature;
Sat, 29 Sep 2012 16:15:18 +0200 wenzelm treat wrapped markup elements as raw markup delimiters;
Wed, 07 Mar 2012 23:21:24 +0100 wenzelm tuned message (cf. ML version);
Wed, 07 Mar 2012 20:49:18 +0100 wenzelm eliminated dead code;
Sun, 04 Sep 2011 15:21:50 +0200 wenzelm moved XML/YXML to src/Pure/PIDE;
less more (0) tip