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;
theory Syntax
imports Base
begin
chapter {* Concrete syntax and type-checking *}
text FIXME
section {* Parsing and printing *}
text FIXME
section {* Checking and unchecking \label{sec:term-check} *}
end