# HG changeset patch
# User wenzelm
# Date 1237129183 -3600
# Node ID 7f9a9ec1c94d8c0e748629472b24632b691db39d
# Parent  8a5a0aa30e1c1df43fe65bdfc4703825b5a879a0
added 'attribute_setup' command;

diff -r 8a5a0aa30e1c -r 7f9a9ec1c94d doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sun Mar 15 15:59:43 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Mar 15 15:59:43 2009 +0100
@@ -800,6 +800,7 @@
     @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
   \begin{mldecls}
@@ -812,6 +813,8 @@
     ;
     ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
     ;
+    'attribute\_setup' name '=' text text
+    ;
   \end{rail}
 
   \begin{description}
@@ -856,6 +859,34 @@
   invoke local theory specification packages without going through
   concrete outer syntax, for example.
 
+  \item @{command "attribute_setup"}~@{text "name = text description"}
+  defines an attribute in the current theory.  The given @{text
+  "text"} has to be an ML expression of type
+  @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
+  structure @{ML_struct Args} and @{ML_struct Attrib}.
+
+  In principle, attributes can operate both on a given theorem and the
+  implicit context, although in practice only one is modified and the
+  other serves as parameter.  Here are examples for these two cases:
+
+  \end{description}
+*}
+
+    attribute_setup my_rule = {*
+      Attrib.thms >> (fn ths =>
+        Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
+          let val th' = th OF ths
+          in th' end)) *}  "my rule"
+
+    attribute_setup my_declatation = {*
+      Attrib.thms >> (fn ths =>
+        Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
+          let val context' = context
+          in context' end)) *}  "my declaration"
+
+text {*
+  \begin{description}
+
   \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
   theorems produced in ML both in the theory context and the ML
   toplevel, associating it with the provided name.  Theorems are put
diff -r 8a5a0aa30e1c -r 7f9a9ec1c94d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 15 15:59:43 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 15 15:59:43 2009 +0100
@@ -328,6 +328,11 @@
     (P.ML_source >> IsarCmd.local_setup);
 
 val _ =
+  OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl)
+    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
+    >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+
+val _ =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
     (P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
     >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));