src/Pure/config.ML
2012-04-27 wenzelm 2012-04-27 avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
2010-10-30 wenzelm 2010-10-30 support for real valued configuration options;
2010-09-06 wenzelm 2010-09-06 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
2010-09-03 wenzelm 2010-09-03 more explicit Config.declare vs. Config.declare_global;
2010-08-27 wenzelm 2010-08-27 tuned printed type names, according to ML;
2010-05-10 wenzelm 2010-05-10 renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-03-28 wenzelm 2010-03-28 pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
2010-03-28 wenzelm 2010-03-28 configuration options admit dynamic default values;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2007-08-02 wenzelm 2007-08-02 added name_of;
2007-08-01 wenzelm 2007-08-01 renamed config_option.ML to config.ML; moved attrib setup to attrib.ML;
2007-07-27 wenzelm 2007-07-27 map_value: dynamic type checking;
2007-07-27 wenzelm 2007-07-27 exported datatype value; added the_config; removed put_generic_src -- moved value parsing to attrib.ML; tuned;
2007-07-25 wenzelm 2007-07-25 Configuration options as values within the local context.