src/Pure/Syntax/syntax.ML
2013-03-29 wenzelm 2013-03-29 Pretty.item markup for improved readability of lists of items;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-01 wenzelm 2012-10-01 report sort assignment of visible type variables;
2012-03-17 wenzelm 2012-03-17 added Syntax.read_typs; tuned parallelism for syntax operations;
2012-03-09 wenzelm 2012-03-09 tuned signature;
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-02-15 wenzelm 2012-02-15 renamed "xstr" to "str_token";
2012-01-16 wenzelm 2012-01-16 position constraints for numerals enable PIDE markup;
2012-01-05 wenzelm 2012-01-05 discontinued Syntax.positions -- atomic parse trees are always annotated;
2011-12-01 wenzelm 2011-12-01 renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
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-25 wenzelm 2011-11-25 prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;
2011-11-14 wenzelm 2011-11-14 inner syntax positions for string literals;
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
2011-11-09 wenzelm 2011-11-09 tuned signature -- emphasize internal role of these operations;
2011-09-07 wenzelm 2011-09-07 explicit join_syntax ensures command transaction integrity of 'theory';
2011-08-10 wenzelm 2011-08-10 future_job: explicit indication of interrupts;
2011-08-06 kleing 2011-08-06 make syntax ambiguity warnings a config option
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-27 wenzelm 2011-06-27 parallel Syntax.parse, which is rather slow;
2011-05-15 wenzelm 2011-05-15 future merge of grammars, to improve parallel performance;
2011-04-26 wenzelm 2011-04-26 clarified auxiliary structure Lexicon.Syntax;
2011-04-19 wenzelm 2011-04-19 explicit markup for loose bounds;
2011-04-19 wenzelm 2011-04-19 slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
2011-04-19 wenzelm 2011-04-19 simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-17 wenzelm 2011-04-17 provide structure Syntax early (before structure Type), back-patch check/uncheck later;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
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 discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 wenzelm 2011-04-08 simplified Pure syntax bootstrap;
2011-04-08 wenzelm 2011-04-08 renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;
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 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-07 wenzelm 2011-04-07 tuned signature;
2011-04-07 wenzelm 2011-04-07 discontinued user-defined token translations; tuned signature;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-04-06 wenzelm 2011-04-06 type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
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 explicit Syntax.tokenize, Syntax.parse;
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-05 wenzelm 2011-04-05 moved decode/parse operations to standard_syntax.ML; tuned;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Parser -- directly accessible;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-05 wenzelm 2011-04-05 more precise propagation of reports/results through some inner syntax layers; misc reorganization;
2011-04-04 wenzelm 2011-04-04 misc tuning and clarification;
2011-04-04 wenzelm 2011-04-04 direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
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-03-27 wenzelm 2011-03-27 tuned signatures;
2011-03-27 wenzelm 2011-03-27 decode_term/disambig: report resolved term variables for the unique (!) result;
2011-03-22 wenzelm 2011-03-22 enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;
2011-03-22 wenzelm 2011-03-22 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;