# HG changeset patch # User wenzelm # Date 1185394850 -7200 # Node ID aa46577f4f4445b538557f2ce04f88075b405e9c # Parent 6d78feed74dd545daf5c08da962b9d4efa4ed916 added attribute "option" for setting configuration options; diff -r 6d78feed74dd -r aa46577f4f44 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Jul 25 22:20:49 2007 +0200 +++ b/src/Pure/Isar/attrib.ML Wed Jul 25 22:20:50 2007 +0200 @@ -185,6 +185,13 @@ (** basic attributes **) +(* configuration options *) + +fun option x = + syntax (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.name)) + >> (fn (name, value) => Thm.declaration_attribute (K (Config.put_generic_src name value)))) x; + + (* tags *) fun tagged x = syntax (tag >> PureThy.tag) x; @@ -264,7 +271,8 @@ val _ = Context.add_setup (add_attributes - [("tagged", tagged, "tagged theorem"), + [("option", option, "named configuration option"), + ("tagged", tagged, "tagged theorem"), ("untagged", untagged, "untagged theorem"), ("kind", kind, "theorem kind"), ("COMP", COMP_att, "direct composition with rules (no lifting)"),