reactivated -segprot options, just to make double-sure;

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;

tuned signature;

simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);

proper range for hyperlinks and tooltips, using original markup information;

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;

Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;

Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;

tuned signatures;

Command.State: accumulate markup reports uniformly; Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo; tuned;

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

added Text.Range.- convenience;

tuned signatures;

alternative constructor for Range singularities;

concentrate protocol message formats in Isar_Document;

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

further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;

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;

updated some isatest settings;

added generated file;

merged

tuned quotes

more antiquotations

deglobalized named HOL constants