src/Pure/Syntax/syntax.ML
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;
2011-03-21 wenzelm 2011-03-21 tuned;
2011-03-21 wenzelm 2011-03-21 clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
2011-02-05 wenzelm 2011-02-05 more tracing information via Par_List.map_name;
2010-12-21 wenzelm 2010-12-21 configuration option "syntax_ast_trace" and "syntax_ast_stat";
2010-12-04 wenzelm 2010-12-04 added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;
2010-09-20 wenzelm 2010-09-20 added XML.content_of convenience -- cover XML.body, which is the general situation;
2010-09-17 wenzelm 2010-09-17 Syntax.read_asts error: report token ranges within message -- no side-effect here;
2010-09-17 wenzelm 2010-09-17 simplified some internal flags using Config.T instead of full-blown Proof_Data;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-09-07 wenzelm 2010-09-07 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase; tuned color;
2010-09-06 wenzelm 2010-09-06 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
2010-09-05 wenzelm 2010-09-05 turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;
2010-09-05 wenzelm 2010-09-05 Syntax.standard_parse_term: eliminated redundant Pretty.pp;
2010-09-05 wenzelm 2010-09-05 structure Syntax: define "interfaces" before actual implementations;
2010-09-03 wenzelm 2010-09-03 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
2010-08-27 wenzelm 2010-08-27 more careful treatment of context visibility flag wrt. spurious warnings;
2010-08-08 wenzelm 2010-08-08 proper context for Syntax.parse_token;
2010-08-08 wenzelm 2010-08-08 prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
2010-08-07 wenzelm 2010-08-07 more robust treatment of Markup.token;
2010-08-07 wenzelm 2010-08-07 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-07-02 wenzelm 2010-07-02 standard argument order; tuned;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-08 wenzelm 2010-05-08 back-patching via Single_Assignment.var;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-19 wenzelm 2010-04-19 update_syntax: add new productions only once, to allow repeated local notation, for example;
2010-03-09 wenzelm 2010-03-09 simplified Syntax.basic_syntax (again); separate Syntax.type_ast_trs depending on read_class/read_type;
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
2010-03-01 wenzelm 2010-03-01 more uniform treatment of syntax for types vs. consts;
2010-02-27 wenzelm 2010-02-27 parallel brute-force disambiguation;
2010-02-21 wenzelm 2010-02-21 filter out authentic const syntax;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2010-02-11 wenzelm 2010-02-11 added ML antiquotation @{syntax_const};
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-29 wenzelm 2009-11-29 tuned message;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-01 wenzelm 2009-03-01 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2008-12-17 haftmann 2008-12-17 dropped Ids
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-11-29 nipkow 2008-11-29 New lexical item "float".
2008-11-18 wenzelm 2008-11-18 tuned;
2008-09-29 wenzelm 2008-09-29 report_token/parse_token: back to context-less version;
2008-09-29 wenzelm 2008-09-29 ContextPosition.report; parse_token/report_token: explicit context;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-08-15 wenzelm 2008-08-15 read_asts: Lexicon.report_token, filter Lexicon.is_proper; report tokens;
2008-08-10 wenzelm 2008-08-10 added parse_token (from proof_context.ML);
2008-08-09 wenzelm 2008-08-09 read_asts: report literal tokens;
2008-08-09 wenzelm 2008-08-09 read_token: more robust handling of empty text;
2008-08-07 wenzelm 2008-08-07 added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;