2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-01 wenzelm 2016-04-01 required space is already part of;
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-04-01 wenzelm 2016-04-01 clarified end position;
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-03-29 wenzelm 2016-03-29 proper norm_props, e.g. relevant for ML pp;
2016-03-06 wenzelm 2016-03-06 clarified treatment of fragments of Isabelle symbols during bootstrap;
2014-12-03 wenzelm 2014-12-03 clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete \<^sync> marker;
2014-08-11 wenzelm 2014-08-11 clarified signature: entity serial number is not position id;
2014-04-11 wenzelm 2014-04-11 tuned message, to accommodate extra brackets produced by Scala parsers;
2014-04-08 wenzelm 2014-04-08 no report for position singularity, notably for aux. file, especially empty one;
2014-04-06 wenzelm 2014-04-06 clarified position: no offset here;
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-06 wenzelm 2014-03-06 more decisive commitment to get_free vs. the_const; tuned;
2014-03-05 wenzelm 2014-03-05 more markup for inner syntax class/type names (notably for completion); explicit reports result without broadcast yet, which is important for brute-force disambiguation;
2014-02-20 wenzelm 2014-02-20 tuned messages;
2014-02-17 wenzelm 2014-02-17 always show PIDE positions as \<here> (0x002302 "House" from DejaVuSansMono);
2013-10-02 wenzelm 2013-10-02 tuned;
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2012-11-28 wenzelm 2012-11-28 prefer tight Markup.print_int/parse_int for property values;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-03 wenzelm 2012-10-03 more error positions;
2012-09-22 wenzelm 2012-09-22 report proper binding positions only -- avoid swamping document model with unspecific information;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to;
2012-08-11 wenzelm 2012-08-11 reports with body text, not just markup;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-08 wenzelm 2011-11-08 entity markup for bound variables;
2011-09-06 wenzelm 2011-09-06 bulk reports for improved message throughput;
2011-09-06 wenzelm 2011-09-06 tuned signature;
2011-08-16 wenzelm 2011-08-16 tuned message;
2011-08-15 wenzelm 2011-08-15 tuned error message;
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-05-15 wenzelm 2011-05-15 timing of Theory_Data operations, with implicit thread positions when functor is applied;
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-04-03 wenzelm 2011-04-03 added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;
2011-01-11 wenzelm 2011-01-11 clarified notion Position.is_reported; ML warning/error: retain non-reported clear-text position, notably when evaluating external ML files;
2011-01-09 wenzelm 2011-01-09 more direct treatment of Position.end_offset; tuned;
2011-01-09 wenzelm 2011-01-09 discontinued unused end_line, end_column;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_) variants;
2010-09-17 wenzelm 2010-09-17 simplified/clarified (Context_)Position.markup/reported_text;
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-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. (useful markup);
2010-06-24 wenzelm 2010-06-24 explicit treatment of UTF8 character sequences as Isabelle symbols;
2010-05-21 wenzelm 2010-05-21 more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
2009-10-24 wenzelm 2009-10-24 maintain position of formal entities via name space;
2009-09-15 wenzelm 2009-09-15 Isar.define_command: identify transaction;
2009-07-25 wenzelm 2009-07-25 eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;
2009-06-04 wenzelm 2009-06-04 export file_name;
2009-06-04 wenzelm 2009-06-04 export value;
2009-03-23 wenzelm 2009-03-23 added report_text -- status messages with text body;
2009-01-02 wenzelm 2009-01-02 added id; tuned;
2008-09-04 wenzelm 2008-09-04 Thread.getLocal/setLocal;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-09 wenzelm 2008-08-09 added distance_of (permissive version); added no_range; tuned;
2008-08-08 wenzelm 2008-08-08 count offset as well; more uniform treatment of invalid fields; tuned;
2008-08-08 wenzelm 2008-08-08 made SML/NJ happy;
2008-08-07 wenzelm 2008-08-07 only increment column if valid; more robust handling of invalid entries; clarified line/line_file: no column here; added start = (1, 1); added reset_range; tuned;
2008-08-07 wenzelm 2008-08-07 advance: single argument (again); added range; tuned;