src/Pure/consts.ML
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-29 ago renamed Position.str_of to Position.here;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2011-11-28 ago separate module for concrete Isabelle markup;
2011-07-13 ago sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
2011-06-25 ago entity markup for "type", "constant";
2011-04-23 ago clarified Consts.read_const;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-17 ago added Binding.print convenience, which includes quote already;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-03-24 ago added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2010-12-17 ago extra checking of name bindings for classes, types, consts;
2010-11-26 ago make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-03-09 ago aliases for class/type/const;
2010-03-03 ago added extern_syntax;
2010-02-21 ago slightly more abstract syntax mark/unmark operations;
2010-02-21 ago authentic syntax for *all* term constants;
2009-11-01 ago adapted Item_Net;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago conceal consts via name space, not tags;
2009-10-24 ago maintain position of formal entities via name space;
2009-10-24 ago maintain explicit name space kind;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 ago eliminated redundant bindings;
2009-07-09 ago renamed structure TermSubst to Term_Subst;
2009-03-17 ago strip_abss: always strip abstractions as far as possible, without keeping alternatives (which appear to be redundant anyway, but cause significant slowdown since discrimination nets collapse abstractions);
2009-03-17 ago reverted abbreviations: improved performance via Item_Net.T;
2009-03-12 ago renamed NameSpace.bind to NameSpace.define;
2009-03-10 ago Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
2009-03-05 ago eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-01-21 ago removed Ids;
2009-01-21 ago binding is alias for Binding.T
2008-12-30 ago Temporarily avoid type errors in parse phase.
2008-12-04 ago cleaned up binding module and related code
2008-11-20 ago using name bindings
2008-08-27 ago type Properties.T;
2008-02-10 ago maintain default position;
2007-11-11 ago simplified Consts.dest;
2007-11-11 ago renamed Symtab.update_list to Symtab.cons_list;
2007-10-20 ago PrintMode.internal;
2007-10-16 ago the_abbreviation: return plain rhs only;
2007-10-15 ago renamed the_declaration to the_type;
2007-10-15 ago prefer first constant component on merge
2007-10-12 ago (intermediate quickfix)
2007-10-08 ago maintain typargs for abbrevs as well;
2007-09-30 ago maintain tags (Markup.property list);
2007-09-22 ago certify: do_expand as explicit argument, actually certify type of abstractions;
2007-07-08 ago replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-05-24 ago tuned Pure/General/name_space.ML
2007-04-02 ago exception handling
2006-12-13 ago tuned;
2006-12-12 ago abbreviate: tuned signature;
2006-12-09 ago abbreviate: always authentic, force expansion of internal abbreviations;