2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-01 ago tuned signature;
2014-03-01 ago clarified language markup: added "delimited" property;
2013-05-26 ago tuned signature;
2013-05-25 ago syntax translations always depend on context;
2013-04-04 ago added var_position in analogy to longid_position, for typing reports on input;
2013-03-29 ago Pretty.item markup for improved readability of lists of items;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-01 ago report sort assignment of visible type variables;
2012-03-17 ago added Syntax.read_typs;
2012-03-09 ago tuned signature;
2012-02-17 ago simplified configuration options for syntax ambiguity;
2012-02-16 ago simplified configuration options for syntax ambiguity;
2012-02-15 ago renamed "xstr" to "str_token";
2012-01-16 ago position constraints for numerals enable PIDE markup;
2012-01-05 ago discontinued Syntax.positions -- atomic parse trees are always annotated;
2011-12-01 ago renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-25 ago removed obsolete argument (cf. 954e9d6782ea);
2011-11-25 ago prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
2011-11-14 ago inner syntax positions for string literals;
2011-11-09 ago tuned signature;
2011-11-09 ago tuned signature -- emphasize internal role of these operations;
2011-09-07 ago explicit join_syntax ensures command transaction integrity of 'theory';
2011-08-10 ago future_job: explicit indication of interrupts;
2011-08-06 ago make syntax ambiguity warnings a config option
2011-07-10 ago inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
2011-06-27 ago parallel Syntax.parse, which is rather slow;
2011-05-15 ago future merge of grammars, to improve parallel performance;
2011-04-26 ago clarified auxiliary structure Lexicon.Syntax;
2011-04-19 ago explicit markup for loose bounds;
2011-04-19 ago slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
2011-04-19 ago simplified check/uncheck interfaces: result comparison is hardwired by default;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-17 ago provide structure Syntax early (before structure Type), back-patch check/uncheck later;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago more accurate markup for syntax consts, notably binders which point back to the original logical entity;
2011-04-08 ago discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 ago simplified Pure syntax bootstrap;
2011-04-08 ago renamed sprop "prop#" to "prop'" -- proper identifier;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-04-08 ago discontinued special status of structure Printer;
2011-04-08 ago discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
2011-04-08 ago discontinued special treatment of structure Mixfix;
2011-04-08 ago explicit structure Syntax_Trans;
2011-04-07 ago tuned signature;
2011-04-07 ago discontinued user-defined token translations;
2011-04-06 ago separate structure Term_Position;
2011-04-06 ago type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
2011-04-06 ago eliminated slightly odd Syntax.rep_syntax;
2011-04-06 ago more abstract print translation;
2011-04-06 ago more abstract syntax translation;
2011-04-06 ago explicit Syntax.tokenize, Syntax.parse;
2011-04-06 ago typed_print_translation: discontinued show_sorts argument;
2011-04-06 ago moved unparse material to syntax_phases.ML;
2011-04-05 ago moved decode/parse operations to standard_syntax.ML;
2011-04-05 ago discontinued special treatment of structure Parser -- directly accessible;
2011-04-05 ago discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-05 ago more precise propagation of reports/results through some inner syntax layers;
2011-04-04 ago misc tuning and clarification;