2014-08-13 wenzelm 2014-08-13 tuned;
2014-08-12 wenzelm 2014-08-12 clarified Position.Identified: do not require range from prover, default to command position;
2014-08-12 wenzelm 2014-08-12 maintain Command_Range position as in ML;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-11 wenzelm 2014-04-11 tuned message, to accommodate extra brackets produced by Scala parsers;
2014-04-08 wenzelm 2014-04-08 simplified Text.Chunk -- eliminated ooddities; afford strict symbol_index, which is usually empty anyway;
2014-04-08 wenzelm 2014-04-08 tuned signature -- moved Command.Chunk to Text.Chunk;
2014-04-08 wenzelm 2014-04-08 more precise token positions;
2014-04-08 wenzelm 2014-04-08 more explicit Command.Chunk types, less ooddities; tuned;
2014-03-03 wenzelm 2014-03-03 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
2014-02-18 wenzelm 2014-02-18 prefer concrete list append;
2014-02-14 wenzelm 2014-02-14 updated thy_info.dependencies;
2014-02-11 wenzelm 2014-02-11 report (but ignore) markup within auxiliary files;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-09-18 wenzelm 2012-09-18 pass base_snapshot to enable hyperlinks into other nodes; clarified "def" positions: refrain from renaming properties; clarified snapshot.is_output vs. output and hyperlinks;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to;
2012-08-24 wenzelm 2012-08-24 tuned signature;
2012-07-27 wenzelm 2012-07-27 simplified Path vs. JVM File operations;
2012-07-20 wenzelm 2012-07-20 more explicit{File => JFile};
2012-07-20 wenzelm 2012-07-20 require explicit initialization of options; more explicit Position operations;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-07-12 wenzelm 2011-07-12 more uniform Properties in ML and Scala;
2011-07-08 wenzelm 2011-07-08 discontinued odd Position.column -- left-over from attempts at PGIP implementation; Position.offset discriminates postions precisely, now also available for Position.line/line_file;
2011-04-11 wenzelm 2011-04-11 Name_Space.entry_markup: keep def position as separate properties; uniform treatment of ML_def/ML_open/ML_struct as entities; hyperlinks for all entities -- excluding ML_open/ML_struct for now;
2011-01-09 wenzelm 2011-01-09 discontinued unused end_line, end_column;
2010-09-02 wenzelm 2010-09-02 Position.Range: exclude singularity (again);
2010-08-31 wenzelm 2010-08-31 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;
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.