src/Pure/General/yxml.scala
Thu, 06 May 2010 17:49:57 +0200 wenzelm misc tuning -- accumulate body via ListBuffer;
Mon, 28 Dec 2009 22:03:14 +0100 wenzelm separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
Mon, 28 Dec 2009 18:40:13 +0100 wenzelm moved Library.decode_permissive_utf8 to Isabelle_System;
Sun, 27 Dec 2009 23:09:16 +0100 wenzelm factored-out Library.decode_permissive_utf8;
Fri, 18 Dec 2009 12:28:50 +0100 wenzelm markup bad YXML as malformed;
Fri, 18 Dec 2009 12:10:52 +0100 wenzelm replace invalid code points -- instead of exception;
Thu, 17 Dec 2009 20:09:19 +0100 wenzelm added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
Sat, 29 Aug 2009 14:31:39 +0200 wenzelm misc tuning;
Tue, 09 Jun 2009 20:18:21 +0200 wenzelm tuned;
Fri, 05 Jun 2009 21:55:08 +0200 wenzelm removed obsolete YXML/XML.detect;
Mon, 19 Jan 2009 16:03:04 +0100 wenzelm intern names of elements and attributes;
Fri, 16 Jan 2009 22:54:11 +0100 wenzelm added parse_body_failsafe;
Sat, 27 Dec 2008 17:09:27 +0100 wenzelm tuned;
Fri, 19 Dec 2008 20:37:29 +0100 wenzelm removed Ids;
Mon, 25 Aug 2008 20:01:17 +0200 wenzelm simplified exceptions: use plain error function / RuntimeException;
Sat, 23 Aug 2008 23:07:41 +0200 wenzelm renamed Markup.MALFORMED to Markup.BAD;
Sat, 23 Aug 2008 19:42:14 +0200 wenzelm added parse_failsafe;
Thu, 21 Aug 2008 22:06:17 +0200 wenzelm parse_attrib: proper index of name end!
Thu, 21 Aug 2008 21:42:16 +0200 wenzelm tuned parse performance: avoid splitting terminal Y chunk;
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