src/Pure/PIDE/xml.scala
13 months ago wenzelm 2018-05-13 tuned signature;
15 months ago wenzelm 2018-03-11 tuned;
15 months ago wenzelm 2018-03-11 convenience to represent XML.Body as single XML.Elem;
18 months ago wenzelm 2017-12-01 more operations;
18 months ago wenzelm 2017-12-01 proper synchronized Map: this may be used on multiple threads;
24 months ago wenzelm 2017-06-26 some HTML GUI elements;
2017-06-01 wenzelm 2017-06-01 tuned;
2017-06-01 wenzelm 2017-06-01 uniform output of HTML as XML; discontinued special cases of 041dc6d8d344;
2017-05-22 wenzelm 2017-05-22 clarified signature;
2017-05-08 wenzelm 2017-05-08 proper type for iterated application;
2017-05-07 wenzelm 2017-05-07 more operations; tuned;
2017-03-20 wenzelm 2017-03-20 tuned;
2017-03-20 wenzelm 2017-03-20 more operations;
2017-01-07 wenzelm 2017-01-07 Line.Document consists of independently allocated strings; tuned signature;
2016-10-24 wenzelm 2016-10-24 discontinued unused / untested distinction of separate PIDE modules;
2016-10-23 wenzelm 2016-10-23 more operations (see also properties.ML);
2016-10-23 wenzelm 2016-10-23 tuned;
2015-08-26 wenzelm 2015-08-26 tuned signature;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2014-08-12 wenzelm 2014-08-12 tuned;
2014-08-12 wenzelm 2014-08-12 more compact representation of special string values;
2014-02-20 wenzelm 2014-02-20 tuned imports;
2013-08-07 wenzelm 2013-08-07 tuned signature; tuned;
2013-05-14 wenzelm 2013-05-14 tuned signature;
2013-04-09 wenzelm 2013-04-09 tuned signature;
2013-02-19 wenzelm 2013-02-19 help JVM to cope with large symbolic structures;
2012-09-28 wenzelm 2012-09-28 support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-27 wenzelm 2012-09-27 removed obsolete org.w3c.dom operations;
2012-09-20 wenzelm 2012-09-20 tuned signature;
2012-09-20 wenzelm 2012-09-20 tuned;
2012-09-18 wenzelm 2012-09-18 recover order of stacked markup;
2012-09-18 wenzelm 2012-09-18 some actual rich text markup via XML.content_markup; tuned signature;
2012-03-08 wenzelm 2012-03-08 simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
2011-11-29 wenzelm 2011-11-29 separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-28 wenzelm 2011-11-28 explicit indication of modules for independent Scala library;
2011-09-07 wenzelm 2011-09-07 XML.cache for partial sharing (strings only);
2011-09-05 wenzelm 2011-09-05 tuned imports;
2011-09-04 wenzelm 2011-09-04 simplified signatures;
2011-09-04 wenzelm 2011-09-04 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
2011-09-04 wenzelm 2011-09-04 moved XML/YXML to src/Pure/PIDE; tuned comments;