2014-11-08 wenzelm 2014-11-08 removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
2014-08-05 wenzelm 2014-08-05 refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-05-16 wenzelm 2013-05-16 tuned signature;
2013-05-14 wenzelm 2013-05-14 more uniform Markup.print_real;
2013-05-12 wenzelm 2013-05-12 support for system options as context-sensitive config options;
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.