src/Pure/Syntax/syntax_phases.ML
2012-10-01 wenzelm 2012-10-01 report sort assignment of visible type variables;
2012-09-29 wenzelm 2012-09-29 proper handling of constraints stemming from idtyp_ast_tr';
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-09-29 wenzelm 2012-09-29 explicit show_types takes preferenced over show_markup;
2012-09-29 wenzelm 2012-09-29 turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;
2012-09-29 wenzelm 2012-09-29 tuned signature;
2012-09-14 wenzelm 2012-09-14 clarified markup names;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-11 wenzelm 2012-08-11 clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
2012-08-10 wenzelm 2012-08-10 sneak message into "bad" markup as property -- to be displayed after YXML parsing;
2012-08-10 wenzelm 2012-08-10 more visible markup of malformed input as "bad";
2012-03-17 wenzelm 2012-03-17 added Syntax.read_typs; tuned parallelism for syntax operations;
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;