src/Pure/PIDE/yxml.ML
2012-09-29 wenzelm 2012-09-29 treat wrapped markup elements as raw markup delimiters;
2012-03-07 wenzelm 2012-03-07 tuned message (cf. ML version);
2012-03-07 wenzelm 2012-03-07 eliminated dead code; tuned;
2011-09-04 wenzelm 2011-09-04 moved XML/YXML to src/Pure/PIDE; tuned comments;