src/Pure/PIDE/markup_tree.scala
2016-10-24 ago discontinued unused / untested distinction of separate PIDE modules;
2015-05-03 ago misc tuning, based on warnings by IntelliJ IDEA;
2014-09-26 ago tuned message;
2014-08-12 ago tuned;
2014-04-29 ago more systematic Isabelle output, like in classic Isabelle/ML (without markup);
2014-04-26 ago tuned signature;
2014-03-29 ago tuned -- see Text.Range.overlaps(Range);
2014-03-28 ago tuned;
2014-03-27 ago more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
2014-03-27 ago more frugal merge of markup trees: non-overlapping tree counts as empty;
2014-03-27 ago more frugal merge of markup trees: filter wrt. subsequent query;
2014-03-27 ago tuned signature;
2014-03-27 ago more careful treatment of multiple command states (eval + prints): merge content that is actually required;
2014-03-01 ago tuned signature -- more explicit Document.Elements;
2014-02-21 ago eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
2014-02-21 ago tuned -- remaining rev_markup is rather short after filter;
2014-02-20 ago clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
2014-02-20 ago cumulate/select wrt. precise elements guard;
2014-02-20 ago tuned imports;
2013-08-07 ago more elementary list structures for markup tree traversal;
2013-08-07 ago more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
2013-07-13 ago full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
2013-04-04 ago tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
2012-12-30 ago ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
2012-12-15 ago maintain subtree_elements for improved performance of cumulate operator;
2012-12-15 ago more formal class Markup_Tree.Elements;
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;