src/Pure/PIDE/yxml.ML
4 months ago ago more scalable on 32-bit Poly/ML;
14 months ago ago more scalable;
2016-10-17 ago accomodate Poly/ML repository version, which treats singleton strings as boxed;
2015-01-24 ago tuned signature;
2012-09-29 ago treat wrapped markup elements as raw markup delimiters;
2012-03-07 ago tuned message (cf. ML version);
2012-03-07 ago eliminated dead code;
2011-09-04 ago moved XML/YXML to src/Pure/PIDE;