misc tuning, following hint by IntelliJ;

discontinued unused / untested distinction of separate PIDE modules;

misc tuning, based on warnings by IntelliJ IDEA;

tuned message;

tuned;

more systematic Isabelle output, like in classic Isabelle/ML (without markup);

tuned signature;

tuned -- see Text.Range.overlaps(Range);

tuned;

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);

more frugal merge of markup trees: non-overlapping tree counts as empty;

more frugal merge of markup trees: filter wrt. subsequent query;

tuned signature;

more careful treatment of multiple command states (eval + prints): merge content that is actually required;
more standard Markup_Tree merge, including trivial cases;

tuned signature -- more explicit Document.Elements;

eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);

tuned -- remaining rev_markup is rather short after filter;

clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;

cumulate/select wrt. precise elements guard;
tuned signature;

tuned imports;

more elementary list structures for markup tree traversal;

more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;

full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);

tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;

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);

maintain subtree_elements for improved performance of cumulate operator;

more formal class Markup_Tree.Elements;

support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

operations to turn markup into XML;
tuned;

tuned;

updated to consolidated SortedMap in scala-2.9.x;

more direct Markup_Tree.from_XML;

more direct Markup_Tree.from_XML;

tuned signature;

tuned;

recover order of stacked markup;

tuned message;

flat presentation of collective markup;

prefer final ADTs -- prevent ooddities;

clarified Isabelle_Rendering vs. physical painting;
discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;

proper cumulation of bulk arguments;

separate compilation of PIDE vs. Pure sources, which enables independent Scala library;

explicit indication of modules for independent Scala library;

index markup elements for more efficient cumulate/select operations;

tuned;

more precise type;

refined Markup_Tree implementation: stacked markup within each entry;
tuned;

tuned signature;
express select in terms of cumulate;

tuned signature;

added markup_cumulate operator;

tuned;

more abstract Markup_Tree;

prefer statically typed Text.Markup;

added official Text.Range.Ordering;
some support for text perspective;

tuned signature;

explicit import java.lang.System to prevent odd scope problems;

concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;

simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
tuned Snapshot.convert/revert;

added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
Markup_Tree.select: plain Iterator;
misc tuning and simplification;

Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;

Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;

Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
tuned;

misc tuning of important special cases;

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") *}

tuned signature;

misc tuning and simplification;

renamed Markup_Tree.Node to Text.Info;
Markup_Tree.select: body may depend on full Text.Info, including range;
tuned;

removed obsolete Markup_Tree.flatten/filter;

Markup_Tree.select: misc simplification, proper restriction of parent in subtree;

alternative constructor for Range singularities;

Branches.overlapping: proper treatment of stop_range that overlaps with end;
Markup_Tree.select: allow singularity in parent range specification;

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;

added toString methods;

misc tuning and simplification;

Markup_Tree.select: crude version of stream-based filtering;

tuned Markup_Tree, using SortedMap more carefully;

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;

--HG--
rename : src/Pure/PIDE/markup_node.scala => src/Pure/PIDE/markup_tree.scala