src/Pure/context.ML
Fri, 18 Mar 2016 16:26:35 +0100 wenzelm clarified modules;
Sun, 20 Dec 2015 13:11:47 +0100 wenzelm tuned signature;
Sun, 20 Dec 2015 13:06:26 +0100 wenzelm renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
Fri, 25 Sep 2015 20:04:25 +0200 wenzelm less redundant output;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Mon, 31 Aug 2015 14:16:32 +0200 wenzelm tuned message;
Sun, 30 Aug 2015 15:21:25 +0200 wenzelm clarified exceptions;
Fri, 28 Aug 2015 23:48:03 +0200 wenzelm clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
Fri, 28 Aug 2015 23:21:04 +0200 wenzelm more abstract theory certificate, which is not necessarily the full theory;
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Sun, 16 Aug 2015 17:11:31 +0200 wenzelm separate type theory_id;
Sat, 20 Dec 2014 19:12:41 +0100 wenzelm tuned;
Thu, 18 Dec 2014 15:21:54 +0100 wenzelm avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Mon, 17 Feb 2014 22:39:20 +0100 wenzelm 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);
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Thu, 18 Jul 2013 13:12:54 +0200 wenzelm 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;
Wed, 17 Jul 2013 09:32:08 +0200 wenzelm tuned;
Wed, 10 Apr 2013 17:02:47 +0200 wenzelm added ML antiquotation @{theory_context};
Thu, 07 Mar 2013 15:02:55 +0100 wenzelm tuned signature -- prefer terminology of Scala and Axiom;
Sat, 08 Dec 2012 13:25:49 +0100 wenzelm check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Wed, 01 Aug 2012 19:53:20 +0200 wenzelm more standard bootstrapping of Pure.thy;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Wed, 06 Jul 2011 20:46:06 +0200 wenzelm prefer Synchronized.var;
Thu, 30 Jun 2011 16:50:26 +0200 wenzelm back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
Sun, 15 May 2011 20:38:08 +0200 wenzelm timing of Theory_Data operations, with implicit thread positions when functor is applied;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 05 Feb 2011 20:38:32 +0100 wenzelm more tracing information via Par_List.map_name;
Wed, 01 Sep 2010 15:33:59 +0200 haftmann replaced Table.map' by Table.map
Wed, 21 Jul 2010 15:31:38 +0200 wenzelm replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
Wed, 21 Jul 2010 14:27:05 +0200 wenzelm added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
Tue, 20 Jul 2010 14:44:33 +0200 wenzelm 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;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Mon, 04 Jan 2010 23:20:35 +0100 wenzelm 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);
Mon, 04 Jan 2010 20:25:56 +0100 wenzelm removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
Mon, 04 Jan 2010 14:09:56 +0100 haftmann dropped copy operation for legacy TheoryDataFun
Wed, 11 Nov 2009 00:11:26 +0100 wenzelm local mutex for theory content/identity operations;
Sun, 08 Nov 2009 16:27:50 +0100 wenzelm modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
Tue, 20 Oct 2009 22:46:24 +0200 wenzelm tuned;
Tue, 20 Oct 2009 21:26:45 +0200 wenzelm backpatching of structure Proof and ProofContext -- avoid odd aliases;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 09 Jul 2009 22:01:41 +0200 wenzelm renamed functor TableFun to Table, and GraphFun to Graph;
Sat, 21 Mar 2009 20:00:23 +0100 wenzelm removed obsolete pprint operations;
Tue, 06 Jan 2009 14:43:35 +0100 wenzelm renamed structure ParList to Par_List;
Tue, 06 Jan 2009 14:33:49 +0100 wenzelm parallelized merge_data;
Sat, 13 Dec 2008 15:35:18 +0100 wenzelm tuned comments;
Sat, 13 Dec 2008 15:06:24 +0100 wenzelm refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
Thu, 11 Dec 2008 20:31:45 +0100 wenzelm unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
Sat, 06 Dec 2008 00:08:07 +0100 wenzelm finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
Thu, 16 Oct 2008 22:44:26 +0200 wenzelm tuned;
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Mon, 22 Sep 2008 15:26:11 +0200 wenzelm added reject_draft;
Thu, 04 Sep 2008 16:03:44 +0200 wenzelm Thread.getLocal/setLocal;
Tue, 24 Jun 2008 19:43:17 +0200 wenzelm added pprint_thy_ref;
Sun, 18 May 2008 17:03:20 +0200 wenzelm eliminated theory CPure;
Wed, 14 May 2008 14:43:37 +0200 wenzelm names_of: exclude intermediate ids -- less verbosity;
less more (0) -100 -60 tip