#
a7912ed2 |
|
10-Oct-2019 |
wenzelm <none@none> |
more compact XML representation;
|
#
ecc31254 |
|
05-Mar-2019 |
wenzelm <none@none> |
tuned;
|
#
31cdab66 |
|
14-Feb-2019 |
wenzelm <none@none> |
support for XML name spaces;
|
#
9e9157b4 |
|
14-Feb-2019 |
wenzelm <none@none> |
uniform XML header;
|
#
a370b4a1 |
|
24-May-2018 |
wenzelm <none@none> |
more general cache, also for term substructures;
|
#
8f980f23 |
|
13-May-2018 |
wenzelm <none@none> |
tuned signature;
|
#
bd1bfd88 |
|
11-Mar-2018 |
wenzelm <none@none> |
tuned;
|
#
b2d5a022 |
|
11-Mar-2018 |
wenzelm <none@none> |
convenience to represent XML.Body as single XML.Elem;
|
#
6bc35a98 |
|
01-Dec-2017 |
wenzelm <none@none> |
more operations;
|
#
075f6905 |
|
01-Dec-2017 |
wenzelm <none@none> |
proper synchronized Map: this may be used on multiple threads;
|
#
e496fe49 |
|
26-Jun-2017 |
wenzelm <none@none> |
some HTML GUI elements;
|
#
be5bfae0 |
|
31-May-2017 |
wenzelm <none@none> |
tuned;
|
#
ca3ed849 |
|
01-Jun-2017 |
wenzelm <none@none> |
uniform output of HTML as XML; discontinued special cases of 041dc6d8d344;
|
#
057fcdaf |
|
22-May-2017 |
wenzelm <none@none> |
clarified signature;
|
#
20913e35 |
|
08-May-2017 |
wenzelm <none@none> |
proper type for iterated application;
|
#
bdbe0d84 |
|
07-May-2017 |
wenzelm <none@none> |
more operations; tuned;
|
#
d9adbac2 |
|
20-Mar-2017 |
wenzelm <none@none> |
tuned;
|
#
378e17dd |
|
20-Mar-2017 |
wenzelm <none@none> |
more operations;
|
#
a1afe236 |
|
07-Jan-2017 |
wenzelm <none@none> |
Line.Document consists of independently allocated strings; tuned signature;
|
#
3ee6c0a8 |
|
23-Oct-2016 |
wenzelm <none@none> |
discontinued unused / untested distinction of separate PIDE modules;
|
#
bd848fac |
|
23-Oct-2016 |
wenzelm <none@none> |
more operations (see also properties.ML);
|
#
e68d4265 |
|
22-Oct-2016 |
wenzelm <none@none> |
tuned;
|
#
d46ccda2 |
|
26-Aug-2015 |
wenzelm <none@none> |
tuned signature;
|
#
e0e8cf48 |
|
02-May-2015 |
wenzelm <none@none> |
misc tuning, based on warnings by IntelliJ IDEA;
|
#
268b5fb9 |
|
12-Aug-2014 |
wenzelm <none@none> |
tuned;
|
#
7af44a03 |
|
12-Aug-2014 |
wenzelm <none@none> |
more compact representation of special string values;
|
#
ffd59da7 |
|
20-Feb-2014 |
wenzelm <none@none> |
tuned imports;
|
#
e1b1ac22 |
|
07-Aug-2013 |
wenzelm <none@none> |
tuned signature; tuned;
|
#
6223d8c5 |
|
14-May-2013 |
wenzelm <none@none> |
tuned signature;
|
#
9a807fd8 |
|
09-Apr-2013 |
wenzelm <none@none> |
tuned signature;
|
#
08d9d3de |
|
19-Feb-2013 |
wenzelm <none@none> |
help JVM to cope with large symbolic structures;
|
#
70369ac4 |
|
28-Sep-2012 |
wenzelm <none@none> |
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
|
#
3426198a |
|
27-Sep-2012 |
wenzelm <none@none> |
removed obsolete org.w3c.dom operations;
|
#
0a23cda4 |
|
20-Sep-2012 |
wenzelm <none@none> |
tuned signature;
|
#
397734df |
|
20-Sep-2012 |
wenzelm <none@none> |
tuned;
|
#
e29cff43 |
|
18-Sep-2012 |
wenzelm <none@none> |
recover order of stacked markup;
|
#
603e40fa |
|
18-Sep-2012 |
wenzelm <none@none> |
some actual rich text markup via XML.content_markup; tuned signature;
|
#
cb3698e0 |
|
08-Mar-2012 |
wenzelm <none@none> |
simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
|
#
2ec142c0 |
|
29-Nov-2011 |
wenzelm <none@none> |
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
|
#
2a73801f |
|
28-Nov-2011 |
wenzelm <none@none> |
explicit indication of modules for independent Scala library;
|
#
6ad2f710 |
|
07-Sep-2011 |
wenzelm <none@none> |
XML.cache for partial sharing (strings only);
|
#
8c7c3981 |
|
05-Sep-2011 |
wenzelm <none@none> |
tuned imports;
|
#
88c4ac56 |
|
04-Sep-2011 |
wenzelm <none@none> |
simplified signatures;
|
#
a9d79109 |
|
04-Sep-2011 |
wenzelm <none@none> |
synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
|
#
ec656bb9 |
|
04-Sep-2011 |
wenzelm <none@none> |
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
|