src/Pure/context.ML
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-03-18 wenzelm 2016-03-18 clarified modules; tuned signature;
2015-12-20 wenzelm 2015-12-20 tuned signature;
2015-12-20 wenzelm 2015-12-20 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
2015-09-25 wenzelm 2015-09-25 less redundant output;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2015-08-31 wenzelm 2015-08-31 tuned message;
2015-08-30 wenzelm 2015-08-30 clarified exceptions; more careful treatment of missing context;
2015-08-28 wenzelm 2015-08-28 clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
2015-08-28 wenzelm 2015-08-28 more abstract theory certificate, which is not necessarily the full theory;
2015-08-16 wenzelm 2015-08-16 prefer theory_id operations; tuned signature;
2015-08-16 wenzelm 2015-08-16 separate type theory_id;
2014-12-20 wenzelm 2014-12-20 tuned;
2014-12-18 wenzelm 2014-12-18 avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-02-17 wenzelm 2014-02-17 subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-18 wenzelm 2013-07-18 immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-07-17 wenzelm 2013-07-17 tuned;
2013-04-10 wenzelm 2013-04-10 added ML antiquotation @{theory_context};
2013-03-07 wenzelm 2013-03-07 tuned signature -- prefer terminology of Scala and Axiom;
2012-12-08 wenzelm 2012-12-08 check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure.thy;
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-07-06 wenzelm 2011-07-06 prefer Synchronized.var;
2011-06-30 wenzelm 2011-06-30 back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
2011-05-15 wenzelm 2011-05-15 timing of Theory_Data operations, with implicit thread positions when functor is applied;
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-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-02-05 wenzelm 2011-02-05 more tracing information via Par_List.map_name;
2010-09-01 haftmann 2010-09-01 replaced Table.map' by Table.map
2010-07-21 wenzelm 2010-07-21 replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
2010-07-21 wenzelm 2010-07-21 added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
2010-07-20 wenzelm 2010-07-20 eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that; tuned some error messages;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-01-04 wenzelm 2010-01-04 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 wenzelm 2010-01-04 removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
2010-01-04 haftmann 2010-01-04 dropped copy operation for legacy TheoryDataFun
2009-11-11 wenzelm 2009-11-11 local mutex for theory content/identity operations;
2009-11-08 wenzelm 2009-11-08 modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
2009-10-20 wenzelm 2009-10-20 tuned;
2009-10-20 wenzelm 2009-10-20 backpatching of structure Proof and ProofContext -- avoid odd aliases; renamed transfer_proof to raw_transfer; indicate firm naming conventions for theory, Proof.context, Context.generic;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-03-21 wenzelm 2009-03-21 removed obsolete pprint operations; some explicit pp operations for toplevel pretty printing;
2009-01-06 wenzelm 2009-01-06 renamed structure ParList to Par_List;
2009-01-06 wenzelm 2009-01-06 parallelized merge_data;
2008-12-13 wenzelm 2008-12-13 tuned comments; tuned;
2008-12-13 wenzelm 2008-12-13 refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;
2008-12-11 wenzelm 2008-12-11 unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;
2008-12-06 wenzelm 2008-12-06 finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
2008-10-16 wenzelm 2008-10-16 tuned;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-22 wenzelm 2008-09-22 added reject_draft;
2008-09-04 wenzelm 2008-09-04 Thread.getLocal/setLocal;