2010-08-19 wenzelm 2010-08-19 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;