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-29 wenzelm 2011-03-29 use shared copy of hoare_syntax.ML; misc tuning;
2011-03-29 wenzelm 2011-03-29 Hoare syntax: standard abstraction syntax admits source positions; re-unified some clones (!);
2011-03-26 wenzelm 2011-03-26 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; recovered printing of Hoare assign statements from 45d090186bbe;
2011-03-26 wenzelm 2011-03-26 tuned;
2011-03-26 wenzelm 2011-03-26 dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-03-24 wenzelm 2011-03-24 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
2011-03-22 wenzelm 2011-03-22 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-22 wenzelm 2011-03-22 binder_tr: more informative exception;
2011-03-22 wenzelm 2011-03-22 update_name_tr: more precise handling of explicit constraints, including positions;
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;
2010-10-28 wenzelm 2010-10-28 use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
2010-09-06 wenzelm 2010-09-06 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
2010-09-03 wenzelm 2010-09-03 turned eta_contract into proper configuration option;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-04-29 wenzelm 2010-04-29 uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
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-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2010-02-18 wenzelm 2010-02-18 made SML/NJ happy (again);
2010-02-16 wenzelm 2010-02-16 moved generic update_name to Pure syntax -- not specific to HOL/record;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-21 haftmann 2009-07-21 attempt for more concise setup of non-etacontracting binders
2009-06-10 wenzelm 2009-06-10 reraise exceptions to preserve position information;
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-16 wenzelm 2008-10-16 added translations for SORT_CONSTRAINT tuned;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2007-07-24 wenzelm 2007-07-24 moved exception capture/release to structure Exn;
2007-07-23 wenzelm 2007-07-23 eliminated transform_failure (to avoid critical section for main transactions);
2007-07-17 wenzelm 2007-07-17 moved print_translations from Pure.thy to Syntax/syn_trans.ML;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context; abs/binder_tr: disallow internal names for bounds;
2006-12-10 wenzelm 2006-12-10 abs/binder_tr': support printing of idtdummy;
2006-11-26 wenzelm 2006-11-26 tuned;
2006-07-25 wenzelm 2006-07-25 added variant_abs (from term.ML); tuned;
2006-07-18 wenzelm 2006-07-18 Term.declare_term_names;
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
2006-06-11 wenzelm 2006-06-11 improved treatment of TERM TYPE syntax;
2006-05-05 wenzelm 2006-05-05 added syntax for _type_constraint_;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-03-21 wenzelm 2006-03-21 mark_boundT: produce well-typed term;
2006-02-23 wenzelm 2006-02-23 make SML/NJ happy;
2006-02-22 wenzelm 2006-02-22 removed obsolete meta_conjunction_tr';
2006-02-10 wenzelm 2006-02-10 moved fixedN to lexicon.ML; tuned;
2006-02-06 wenzelm 2006-02-06 added bound_vars;
2006-01-31 wenzelm 2006-01-31 advanced translations: Context.generic;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-22 wenzelm 2005-12-22 prop_tr': proper handling of aprop marked as bound;
2005-12-02 wenzelm 2005-12-02 asts_to_terms: builtin free_fixed translation makes local binders work properly;
2005-11-19 wenzelm 2005-11-19 tuned;
2005-11-09 wenzelm 2005-11-09 tuned;
2005-10-07 wenzelm 2005-10-07 added idtypdummy_ast_tr; removed obsolete k_tr;
2005-09-13 wenzelm 2005-09-13 replaced TRANSLATION_FAIL by EXCEPTION;
2005-06-29 wenzelm 2005-06-29 transform_failure in translation functions: TRANSLATION_FAIL; proper treatment of advanced trfuns: pass thy argument; tuned bigimpl_ast_tr, impl_ast_tr';
2005-03-03 skalberg 2005-03-03 Move towards standard functions.