# 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)"),