src/Pure/General/yxml.ML
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Fri, 02 Jan 2009 22:54:04 +0100 wenzelm Markup.no_output;
Thu, 28 Aug 2008 00:33:09 +0200 wenzelm removed obsolete XML.Output workaround;
Wed, 27 Aug 2008 20:36:23 +0200 wenzelm replaced find_substring by first_field;
Wed, 27 Aug 2008 16:32:48 +0200 wenzelm simplified parse_attrib (find_substring instead of space_explode);
Sun, 17 Aug 2008 21:11:24 +0200 wenzelm removed parse_element -- no longer fits to liberal parse!
Fri, 15 Aug 2008 15:50:50 +0200 wenzelm output_markup: check Markup.is_none;
Sat, 09 Aug 2008 00:09:31 +0200 wenzelm YXML.parse: allow text without markup, potentially empty;
Wed, 16 Apr 2008 17:40:40 +0200 wenzelm tuned;
Thu, 03 Apr 2008 21:23:38 +0200 wenzelm tuned comments;
Thu, 03 Apr 2008 18:42:38 +0200 wenzelm replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
Thu, 03 Apr 2008 16:03:59 +0200 wenzelm Why XML notation?
less more (0) tip