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