src/Pure/PIDE/markup_tree.scala
2012-09-28 ago support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-27 ago operations to turn markup into XML;
2012-09-27 ago tuned;
2012-09-27 ago updated to consolidated SortedMap in scala-2.9.x;
2012-09-20 ago more direct Markup_Tree.from_XML;
2012-09-20 ago more direct Markup_Tree.from_XML;
2012-09-20 ago tuned signature;
2012-09-20 ago tuned;
2012-09-18 ago recover order of stacked markup;
2012-08-10 ago tuned message;
2012-04-18 ago flat presentation of collective markup;
2012-02-27 ago prefer final ADTs -- prevent ooddities;
2012-01-10 ago clarified Isabelle_Rendering vs. physical painting;
2012-01-09 ago proper cumulation of bulk arguments;
2011-11-29 ago separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
2011-11-28 ago explicit indication of modules for independent Scala library;
2011-11-12 ago index markup elements for more efficient cumulate/select operations;
2011-11-12 ago tuned;
2011-11-12 ago more precise type;
2011-11-12 ago refined Markup_Tree implementation: stacked markup within each entry;
2011-11-12 ago tuned signature;
2011-11-12 ago tuned signature;
2011-11-11 ago added markup_cumulate operator;
2011-11-11 ago tuned;
2011-11-11 ago more abstract Markup_Tree;
2011-11-11 ago prefer statically typed Text.Markup;
2011-08-22 ago added official Text.Range.Ordering;
2011-07-09 ago tuned signature;
2011-06-23 ago explicit import java.lang.System to prevent odd scope problems;
2010-09-07 ago concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
2010-09-07 ago simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
2010-08-29 ago added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
2010-08-26 ago Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
2010-08-24 ago Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
2010-08-24 ago Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
2010-08-23 ago misc tuning of important special cases;
2010-08-22 ago tuned Markup_Tree.+ : slightly more expensive version to rebuild rest avoids crash of RedBlack.scala:120 (version Scala 2.8.0), e.g. on the following input:
2010-08-22 ago tuned signature;
2010-08-22 ago misc tuning and simplification;
2010-08-22 ago renamed Markup_Tree.Node to Text.Info;
2010-08-22 ago removed obsolete Markup_Tree.flatten/filter;
2010-08-20 ago Markup_Tree.select: misc simplification, proper restriction of parent in subtree;
2010-08-20 ago alternative constructor for Range singularities;
2010-08-20 ago Branches.overlapping: proper treatment of stop_range that overlaps with end;
2010-08-19 ago parameterized type Markup_Tree.Node;
2010-08-19 ago added toString methods;
2010-08-19 ago misc tuning and simplification;
2010-08-19 ago Markup_Tree.select: crude version of stream-based filtering;
2010-08-19 ago tuned Markup_Tree, using SortedMap more carefully;
2010-08-18 ago more efficient Markup_Tree, based on branches sorted by quasi-order;