src/Pure/consts.ML
2016-08-08 wenzelm 2016-08-08 Item_Net.retrieve_matching requires beta-eta normal form (amending 8976c5bc9e97);
2016-08-01 wenzelm 2016-08-01 more restrictive retrieval of rules for matching instead of unification -- relevant for performance of printing terms;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2014-03-13 wenzelm 2014-03-13 more frugal recording of changes: join merely requires information from one side; tuned;
2014-03-12 wenzelm 2014-03-12 tuned signature;
2014-03-11 wenzelm 2014-03-11 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-09 wenzelm 2014-03-09 unused;
2014-03-06 wenzelm 2014-03-06 reject internal term names outright, and complete consts instead; more general Name_Space.check_reports; more compact Markup.markup_report;
2014-03-06 wenzelm 2014-03-06 clarified treatment of consts -- prefer value-oriented reports;
2014-03-02 wenzelm 2014-03-02 prefer Name_Space.check with its builtin reports (including completion);
2013-01-08 wenzelm 2013-01-08 tuned -- prefer high-level Table.merge with its slightly more conservative update;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-07-13 wenzelm 2011-07-13 sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;
2011-06-25 wenzelm 2011-06-25 entity markup for "type", "constant";
2011-04-23 wenzelm 2011-04-23 clarified Consts.read_const;
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 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2010-12-17 wenzelm 2010-12-17 extra checking of name bindings for classes, types, consts; tuned;
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-03-09 wenzelm 2010-03-09 aliases for class/type/const; tuned;
2010-03-03 wenzelm 2010-03-03 added extern_syntax;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2009-11-01 wenzelm 2009-11-01 adapted Item_Net; tuned;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 conceal consts via name space, not tags;
2009-10-24 wenzelm 2009-10-24 maintain position of formal entities via name space;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-03-17 wenzelm 2009-03-17 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 wenzelm 2009-03-17 reverted abbreviations: improved performance via Item_Net.T;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-10 wenzelm 2009-03-10 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 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
2009-03-05 wenzelm 2009-03-05 eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-30 ballarin 2008-12-30 Temporarily avoid type errors in parse phase.
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-20 haftmann 2008-11-20 using name bindings
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-02-10 wenzelm 2008-02-10 maintain default position;
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest; dest;
2007-11-11 wenzelm 2007-11-11 renamed Symtab.update_list to Symtab.cons_list;
2007-10-20 wenzelm 2007-10-20 PrintMode.internal;
2007-10-16 wenzelm 2007-10-16 the_abbreviation: return plain rhs only; force_expand: expand to plain rhs; added revert_abbrev; tuned;