# HG changeset patch
# User wenzelm
# Date 1243691599 -7200
# Node ID a74ee84288a0a6dd00ff091bef8716ca94baf8e1
# Parent  a16f4d4f5b24f119761483398ad529d6cbc23e8a
eliminated old Attrib.add_attributes (and Attrib.syntax);

diff -r a16f4d4f5b24 -r a74ee84288a0 NEWS
--- a/NEWS	Sat May 30 15:25:46 2009 +0200
+++ b/NEWS	Sat May 30 15:53:19 2009 +0200
@@ -28,9 +28,9 @@
 
 *** ML ***
 
-* Eliminated old Method.add_methods and related cominators for "method
-args".  INCOMPATIBILITY, need to use simplified Method.setup
-introduced in Isabelle2009.
+* Eliminated old Attrib.add_attributes, Method.add_methods and related
+cominators for "args".  INCOMPATIBILITY, need to use simplified
+Attrib/Method.setup introduced in Isabelle2009.
 
 
 
diff -r a16f4d4f5b24 -r a74ee84288a0 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat May 30 15:25:46 2009 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat May 30 15:53:19 2009 +0200
@@ -26,8 +26,6 @@
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
   val crude_closure: Proof.context -> src -> src
-  val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
-  val syntax: attribute context_parser -> src -> attribute
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
     theory -> theory
@@ -87,6 +85,10 @@
     |> Pretty.chunks |> Pretty.writeln
   end;
 
+fun add_attribute name att comment thy = thy |> Attributes.map (fn atts =>
+  #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts)
+    handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup));
+
 
 (* name space *)
 
@@ -147,24 +149,13 @@
   Args.closure src);
 
 
-(* add_attributes *)
-
-fun add_attributes raw_attrs thy =
-  let
-    val new_attrs =
-      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
-    fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs
-      handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
-  in Attributes.map add thy end;
-
-
 (* attribute setup *)
 
-fun syntax scan src (context, th) =
-  let val (f: attribute, context') = Args.syntax "attribute" scan src context
-  in f (context', th) end;
+fun syntax scan = Args.syntax "attribute" scan;
 
-fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
+fun setup name scan =
+  add_attribute name
+    (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
 
 fun attribute_setup name (txt, pos) cmt =
   Context.theory_map (ML_Context.expression pos
@@ -378,8 +369,8 @@
     val name = Sign.full_bname thy bname;
   in
     thy
-    |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),
-      "configuration option")]
+    |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
+      "configuration option"
     |> Configs.map (Symtab.update (name, config))
   end;