src/Pure/General/yxml.scala
Thu, 21 Aug 2008 21:27:07 +0200 wenzelm parse_attrib: more efficient due to indexOf('=');
Thu, 21 Aug 2008 20:53:31 +0200 wenzelm replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
Sun, 17 Aug 2008 21:11:06 +0200 wenzelm Efficient text representation of XML trees.
less more (0) tip