2014-03-01 wenzelm 2014-03-01 tuned signature -- more explicit Document.Elements;
2014-02-21 wenzelm 2014-02-21 eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
2014-02-21 wenzelm 2014-02-21 tuned -- remaining rev_markup is rather short after filter;
2014-02-20 wenzelm 2014-02-20 clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
2014-02-20 wenzelm 2014-02-20 cumulate/select wrt. precise elements guard; tuned signature;
2014-02-20 wenzelm 2014-02-20 tuned imports;
2013-08-07 wenzelm 2013-08-07 more elementary list structures for markup tree traversal;
2013-08-07 wenzelm 2013-08-07 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
2013-07-13 wenzelm 2013-07-13 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 wenzelm 2013-04-04 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
2012-12-30 wenzelm 2012-12-30 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 wenzelm 2012-12-15 maintain subtree_elements for improved performance of cumulate operator;
2012-12-15 wenzelm 2012-12-15 more formal class Markup_Tree.Elements;
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 operations to turn markup into XML; tuned;
2012-09-27 wenzelm 2012-09-27 tuned;
2012-09-27 wenzelm 2012-09-27 updated to consolidated SortedMap in scala-2.9.x;
2012-09-20 wenzelm 2012-09-20 more direct Markup_Tree.from_XML;
2012-09-20 wenzelm 2012-09-20 more direct Markup_Tree.from_XML;
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-08-10 wenzelm 2012-08-10 tuned message;
2012-04-18 wenzelm 2012-04-18 flat presentation of collective markup;
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-01-10 wenzelm 2012-01-10 clarified Isabelle_Rendering vs. physical painting; discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;
2012-01-09 wenzelm 2012-01-09 proper cumulation of bulk arguments;
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-11-12 wenzelm 2011-11-12 index markup elements for more efficient cumulate/select operations;
2011-11-12 wenzelm 2011-11-12 tuned;
2011-11-12 wenzelm 2011-11-12 more precise type;
2011-11-12 wenzelm 2011-11-12 refined Markup_Tree implementation: stacked markup within each entry; tuned;
2011-11-12 wenzelm 2011-11-12 tuned signature; express select in terms of cumulate;
2011-11-12 wenzelm 2011-11-12 tuned signature;
2011-11-11 wenzelm 2011-11-11 added markup_cumulate operator;
2011-11-11 wenzelm 2011-11-11 tuned;
2011-11-11 wenzelm 2011-11-11 more abstract Markup_Tree;
2011-11-11 wenzelm 2011-11-11 prefer statically typed Text.Markup;
2011-08-22 wenzelm 2011-08-22 added official Text.Range.Ordering; some support for text perspective;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2011-06-23 wenzelm 2011-06-23 explicit import java.lang.System to prevent odd scope problems;
2010-09-07 wenzelm 2010-09-07 concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
2010-09-07 wenzelm 2010-09-07 simplified Stream instead of Iterator (again), explicit Option instead of default; tuned Snapshot.convert/revert;
2010-08-29 wenzelm 2010-08-29 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.; plain Iterator; misc tuning and simplification;
2010-08-26 wenzelm 2010-08-26 uniform treatment of root_range wrt. singularities, yielding empty result stream;
2010-08-24 wenzelm 2010-08-24 Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
2010-08-24 wenzelm 2010-08-24 more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree; tuned;
2010-08-23 wenzelm 2010-08-23 misc tuning of important special cases;
2010-08-22 wenzelm 2010-08-22 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: ML {* fun f x = (x + 1, "aaa") *}
2010-08-22 wenzelm 2010-08-22 tuned signature;
2010-08-22 wenzelm 2010-08-22 misc tuning and simplification;
2010-08-22 wenzelm 2010-08-22 renamed Markup_Tree.Node to Text.Info; body may depend on full Text.Info, including range; tuned;
2010-08-22 wenzelm 2010-08-22 removed obsolete Markup_Tree.flatten/filter;
2010-08-20 wenzelm 2010-08-20 misc simplification, proper restriction of parent in subtree;
2010-08-20 wenzelm 2010-08-20 alternative constructor for Range singularities;
2010-08-20 wenzelm 2010-08-20 Branches.overlapping: proper treatment of stop_range that overlaps with end; allow singularity in parent range specification;
2010-08-19 wenzelm 2010-08-19 parameterized type Markup_Tree.Node; allow arbitrary interpretations, not just filtering; renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;
2010-08-19 wenzelm 2010-08-19 added toString methods;
2010-08-19 wenzelm 2010-08-19 misc tuning and simplification;