# HG changeset patch # User wenzelm # Date 1186049189 -7200 # Node ID 913e1fa904fb25e8287ac6cb7615a59df5ab1f30 # Parent 454a0c8957355bf86527f57fa601f6c6224040f4 turned simp_depth_limit into configuration option; tuned register_config; diff -r 454a0c895735 -r 913e1fa904fb src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Aug 02 12:06:28 2007 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Aug 02 12:06:29 2007 +0200 @@ -27,7 +27,7 @@ val crude_closure: Proof.context -> src -> src val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory val print_configs: Proof.context -> unit - val register_config: bstring -> Config.value Config.T -> theory -> theory + val register_config: Config.value Config.T -> theory -> theory val config_bool: bstring -> bool -> bool Config.T * (theory -> theory) val config_int: bstring -> int -> int Config.T * (theory -> theory) val config_string: bstring -> string -> string Config.T * (theory -> theory) @@ -240,17 +240,22 @@ in -fun register_config name config thy = - thy - |> add_attributes - [(name, syntax (Scan.lift (scan_config thy config) >> Morphism.form), "configuration option")] - |> Configs.map (Symtab.update (Sign.full_name thy name, config)); +fun register_config config thy = + let + val bname = Config.name_of config; + val name = Sign.full_name thy bname; + in + thy + |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form), + "configuration option")] + |> Configs.map (Symtab.update (name, config)) + end; fun declare_config make coerce global name default = let val config_value = Config.declare global name (make default); val config = coerce config_value; - in (config, register_config name config_value) end; + in (config, register_config config_value) end; val config_bool = declare_config Config.Bool Config.bool false; val config_int = declare_config Config.Int Config.int false; @@ -344,7 +349,8 @@ (* theory setup *) val _ = Context.add_setup - (add_attributes + (register_config MetaSimplifier.simp_depth_limit_value #> + add_attributes [("tagged", tagged, "tagged theorem"), ("untagged", untagged, "untagged theorem"), ("kind", kind, "theorem kind"),