src/Pure/General/xml.ML
2011-07-13 wenzelm 2011-07-13 XML.pretty with depth limit;
2011-07-12 wenzelm 2011-07-12 made SML/NJ happy;
2011-07-12 wenzelm 2011-07-12 retain some terminology of "XML attributes";
2011-07-12 wenzelm 2011-07-12 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
2011-07-12 wenzelm 2011-07-12 more precise exceptions;
2011-07-12 wenzelm 2011-07-12 tuned XML modules;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-10-25 wenzelm 2010-10-25 explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-09-20 wenzelm 2010-09-20 added XML.content_of convenience -- cover XML.body, which is the general situation;
2010-08-18 wenzelm 2010-08-18 uniform Markup.empty/Markup.Empty in ML and Scala;
2010-08-10 wenzelm 2010-08-10 type XML.body as basic data representation language; tuned;
2010-08-07 wenzelm 2010-08-07 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2009-06-05 wenzelm 2009-06-05 removed obsolete YXML/XML.detect;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-02 wenzelm 2009-01-02 Markup.no_output;
2008-08-28 wenzelm 2008-08-28 removed obsolete XML.Output workaround;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-15 wenzelm 2008-08-15 output_markup: check Markup.is_none;
2008-05-24 wenzelm 2008-05-24 added parse_document (optional unchecked header material); parse: parse_document instead of parse_element;
2008-04-03 wenzelm 2008-04-03 parser: use plain explode, not Symbol.explode!
2008-04-03 wenzelm 2008-04-03 renamed parse_comment_whspc to parse_comments; major parser cleanup -- removed junk comments;
2008-04-03 wenzelm 2008-04-03 further cleanup of XML signature; replaced plain_content by incremental add_content; added stream output;
2008-04-03 wenzelm 2008-04-03 added output_markup (from Tools/isabelle_process.ML); major cleanup of signature;
2008-04-03 wenzelm 2008-04-03 added detect; removed auxiliary buffer_of_tree; tuned;
2008-01-05 wenzelm 2008-01-05 removed unused text_charref, cdata; added plain_content;
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-14 wenzelm 2007-08-14 moved Tools/xml.ML to General/xml.ML (again);
2007-02-17 aspinall 2007-02-17 Clarify comment
2007-02-01 wenzelm 2007-02-01 removed non-modular comment;
2007-01-30 haftmann 2007-01-30 dropped whitespace
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 aspinall 2006-12-05 Type alias for XML content
2006-12-04 aspinall 2006-12-04 Add parse_string for attribute values and other string content
2006-12-03 aspinall 2006-12-03 Add string buffer getter. Add Rawtext constructor to allow XML-escaped strings in tree.
2006-12-03 aspinall 2006-12-03 Type abbreviations for element args and attributes
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2004-09-29 aspinall 2004-09-29 Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.
2004-09-28 aspinall 2004-09-28 Add text_charref to encode a string using character references
2004-09-27 aspinall 2004-09-27 Add newline after CDATA for sake of HaXml
2004-08-18 aspinall 2004-08-18 Add scan_comment_whspc to skip space and comments in PGIP stream
2004-06-29 kleing 2004-06-29 license change to BSD
2004-06-18 wenzelm 2004-06-18 scalable string_of_tree; tuned;
2004-06-12 wenzelm 2004-06-12 Library.translate_string;
2004-06-09 wenzelm 2004-06-09 Scan.this_string;
2004-06-04 berghofe 2004-06-04 Tuned parse_att.
2004-06-01 aspinall 2004-06-01 Add alternative syntax for attributes
2004-05-29 wenzelm 2004-05-29 Scan.this; tuned;
2004-05-10 wenzelm 2004-05-10 tuned;
2004-05-07 aspinall 2004-05-07 Add FIXME note re FAIL (is it fixed yet?)
2004-05-07 aspinall 2004-05-07 Add cdata output. Add tabs in whitespace. Write two strings instead of Library.quote.
2004-04-16 berghofe 2004-04-16 - tuned text function - Replaced quote by Library.quote, since quote now refers to Symbol.quote
2003-09-04 berghofe 2003-09-04 Tried to make parser a bit more standard-conforming.
2002-11-27 berghofe 2002-11-27 Added XML parser (useful for parsing PGIP / PGML).
2001-12-08 wenzelm 2001-12-08 Basic support for XML output.