tuned signature;

clarified signature: more types;

tuned;

tuned signature;

clarified modules;

--HG--
rename : src/HOL/Tools/value.ML => src/HOL/Tools/value_command.ML

removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);

refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;

more source positions;

prefer Context_Position where a context is available;
prefer explicit Context_Position.is_visible -- avoid redundant message composition;
tuned signature;

tuned signature;

tuned signature;

more uniform Markup.print_real;

support for system options as context-sensitive config options;

avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;

support for real valued configuration options;

more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;

more explicit Config.declare vs. Config.declare_global;

tuned printed type names, according to ML;

renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;

pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;

configuration options admit dynamic default values;

adapted Generic_Data, Proof_Data;
tuned;

removed Ids;

added name_of;

renamed config_option.ML to config.ML;
moved attrib setup to attrib.ML;

map_value: dynamic type checking;

exported datatype value;
added the_config;
removed put_generic_src -- moved value parsing to attrib.ML;
tuned;

Configuration options as values within the local context.