src/Pure/PIDE/yxml.ML
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