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;
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_) 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 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;