src/Pure/PIDE/markup_tree.scala
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 Markup_Tree.select: 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.; Markup_Tree.select: plain Iterator; misc tuning and simplification;
2010-08-26 wenzelm 2010-08-26 Markup_Tree.select: 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 Markup_Tree.select: 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; Markup_Tree.select: 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 Markup_Tree.select: 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; Markup_Tree.select: allow singularity in parent range specification;
2010-08-19 wenzelm 2010-08-19 parameterized type Markup_Tree.Node; Markup_Tree.select: 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;
2010-08-19 wenzelm 2010-08-19 Markup_Tree.select: crude version of stream-based filtering;
2010-08-19 wenzelm 2010-08-19 tuned Markup_Tree, using SortedMap more carefully;
2010-08-18 wenzelm 2010-08-18 more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned;