src/HOL/Import/xml.ML
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2008-04-03 wenzelm 2008-04-03 tuned comments;
2007-09-15 haftmann 2007-09-15 fixed title
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2006-02-17 obua 2006-02-17 replaced Symbol.explode by explode
2006-02-17 obua 2006-02-17 use monomorphic sequences / scanners
2006-02-16 obua 2006-02-16 use VectorScannerSeq instead of ListScannerSeq in xml.ML
2006-02-16 obua 2006-02-16 improved scanning
2006-02-15 obua 2006-02-15 fixed bugs, added caching