src/Pure/PIDE/xml.ML
Sun, 18 Oct 2015 21:30:01 +0200 wenzelm tuned signature;
Thu, 20 Aug 2015 13:41:53 +0200 wenzelm precise BinIO, without newline conversion on Windows;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
less more (0) -10 -3 tip