src/Pure/General/position.scala
2010-08-30 wenzelm 2010-08-30 Command.results: ordered by serial number;
2010-08-25 wenzelm 2010-08-25 organized markup properties via apply/unapply patterns;
2010-08-20 wenzelm 2010-08-20 alternative constructor for Range singularities;
2010-08-20 wenzelm 2010-08-20 further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
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;
2010-08-11 wenzelm 2010-08-11 represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
2010-05-06 wenzelm 2010-05-06 basic support for symbolic pretty printing; tuned;
2010-05-05 wenzelm 2010-05-05 simplified via Position extractors;
2009-12-30 wenzelm 2009-12-30 tuned signature;
2009-08-29 wenzelm 2009-08-29 misc tuning;
2009-06-18 wenzelm 2009-06-18 replaced java Properties by pure property lists; added offsets_of;
2008-12-19 wenzelm 2008-12-19 removed Ids;
2008-08-25 wenzelm 2008-08-25 simplified exceptions: use plain error function / RuntimeException;
2008-08-24 wenzelm 2008-08-24 get: allow null;
2008-08-23 wenzelm 2008-08-23 Position properties.