2012-02-17 wenzelm 2012-02-17 simplified configuration options for syntax ambiguity;
2012-02-16 wenzelm 2012-02-16 simplified configuration options for syntax ambiguity;
2012-01-05 wenzelm 2012-01-05 discontinued Syntax.positions -- atomic parse trees are always annotated;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-25 wenzelm 2011-11-25 removed obsolete argument (cf. 954e9d6782ea);
2011-11-11 wenzelm 2011-11-11 discontinued entity text color, notably historic red for classes; tuned entity names;
2011-11-11 wenzelm 2011-11-11 more scalable Proof_Context.prepare_sorts; reverted a97251eea458 -- uniform position constraints independently of accidental source positions (e.g. TTY vs. document);
2011-11-10 wenzelm 2011-11-10 more efficient prepare_sorts -- bypass encoded positions;
2011-11-10 wenzelm 2011-11-10 suppress irrelevant positions;
2011-11-10 wenzelm 2011-11-10 pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
2011-11-10 wenzelm 2011-11-10 tuned signature;
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
2011-11-09 wenzelm 2011-11-09 sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;
2011-11-09 wenzelm 2011-11-09 tuned signature -- emphasize internal role of these operations;
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-28 wenzelm 2011-08-28 tuned positions of ambiguity messages -- less intrusive in IDE view;
2011-08-06 kleing 2011-08-06 make syntax ambiguity warnings a config option
2011-07-13 wenzelm 2011-07-13 sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-07-10 wenzelm 2011-07-10 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;
2011-06-25 wenzelm 2011-06-25 entity markup for "type", "constant";
2011-06-25 wenzelm 2011-06-25 type classes: entity markup instead of old-style token markup;
2011-04-27 wenzelm 2011-04-27 more informative markup for fixed variables (via name space entry); uniform markup for undeclared entities; tuned;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-26 wenzelm 2011-04-26 clarified auxiliary structure Lexicon.Syntax;
2011-04-23 wenzelm 2011-04-23 more precise error positions;
2011-04-19 wenzelm 2011-04-19 less bulky "_position", for improved readability of parse trees;
2011-04-19 wenzelm 2011-04-19 explicit markup for loose bounds;
2011-04-17 wenzelm 2011-04-17 provide structure Syntax early (before structure Type), back-patch check/uncheck later;
2011-04-17 wenzelm 2011-04-17 tuned signature;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 unparse: more accurate markup for syntax consts, notably binders;
2011-04-08 wenzelm 2011-04-08 more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;
2011-04-08 wenzelm 2011-04-08 CONST syntax with positions;
2011-04-08 wenzelm 2011-04-08 moved CONST syntax/translations to their proper place;
2011-04-08 wenzelm 2011-04-08 simplified Pure syntax bootstrap;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 discontinued special status of structure Printer;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-07 wenzelm 2011-04-07 report literal tokens according to parsetree head; some attempts to stack parsetrees in proper order;
2011-04-07 wenzelm 2011-04-07 simplified read_term vs. read_prop;
2011-04-07 wenzelm 2011-04-07 simplified printer context: uniform externing and static token translations;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-04-06 wenzelm 2011-04-06 eliminated slightly odd Syntax.rep_syntax;
2011-04-06 wenzelm 2011-04-06 more abstract print translation;
2011-04-06 wenzelm 2011-04-06 more abstract syntax translation;
2011-04-06 wenzelm 2011-04-06 tuned;
2011-04-06 wenzelm 2011-04-06 explicit Syntax.tokenize, Syntax.parse;
2011-04-06 wenzelm 2011-04-06 eliminated odd object-oriented type_context/term_context; export ProofContext.intern_skolem;
2011-04-06 wenzelm 2011-04-06 simplified standard parse/unparse;
2011-04-06 wenzelm 2011-04-06 discontinued old-style Syntax.constrainC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2011-04-06 wenzelm 2011-04-06 renamed Standard_Syntax to Syntax_Phases;