more compact XML representation;

tuned;

support for XML name spaces;

uniform XML header;

more general cache, also for term substructures;

tuned signature;

tuned;

convenience to represent XML.Body as single XML.Elem;

more operations;

proper synchronized Map: this may be used on multiple threads;

some HTML GUI elements;

tuned;

uniform output of HTML as XML;
discontinued special cases of 041dc6d8d344;

clarified signature;

proper type for iterated application;

more operations;
tuned;

tuned;

more operations;

Line.Document consists of independently allocated strings;
tuned signature;

discontinued unused / untested distinction of separate PIDE modules;

more operations (see also properties.ML);

tuned;

tuned signature;

misc tuning, based on warnings by IntelliJ IDEA;

tuned;

more compact representation of special string values;

tuned imports;

tuned signature;
tuned;

tuned signature;

tuned signature;

help JVM to cope with large symbolic structures;

support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

removed obsolete org.w3c.dom operations;

tuned signature;

tuned;

recover order of stacked markup;

some actual rich text markup via XML.content_markup;
tuned signature;

simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);

separate compilation of PIDE vs. Pure sources, which enables independent Scala library;

explicit indication of modules for independent Scala library;

XML.cache for partial sharing (strings only);

tuned imports;

simplified signatures;

synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;

moved XML/YXML to src/Pure/PIDE;
tuned comments;

--HG--
rename : src/Pure/General/xml.ML => src/Pure/PIDE/xml.ML
rename : src/Pure/General/xml.scala => src/Pure/PIDE/xml.scala
rename : src/Pure/General/yxml.ML => src/Pure/PIDE/yxml.ML
rename : src/Pure/General/yxml.scala => src/Pure/PIDE/yxml.scala