src/Pure/config.ML
Fri, 27 Apr 2012 21:47:47 +0200 wenzelm avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
Sat, 30 Oct 2010 16:33:58 +0200 wenzelm support for real valued configuration options;
Mon, 06 Sep 2010 21:33:19 +0200 wenzelm more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
Fri, 03 Sep 2010 16:09:12 +0200 wenzelm more explicit Config.declare vs. Config.declare_global;
Fri, 27 Aug 2010 17:02:19 +0200 wenzelm tuned printed type names, according to ML;
Mon, 10 May 2010 20:53:06 +0200 wenzelm renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
Sun, 28 Mar 2010 17:43:09 +0200 wenzelm pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
Sun, 28 Mar 2010 16:13:29 +0200 wenzelm configuration options admit dynamic default values;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Thu, 02 Aug 2007 12:06:28 +0200 wenzelm added name_of;
Wed, 01 Aug 2007 16:55:42 +0200 wenzelm renamed config_option.ML to config.ML;
Fri, 27 Jul 2007 20:11:47 +0200 wenzelm map_value: dynamic type checking;
Fri, 27 Jul 2007 16:31:14 +0200 wenzelm exported datatype value;
Wed, 25 Jul 2007 22:20:49 +0200 wenzelm Configuration options as values within the local context.
less more (0) tip