eliminated old Attrib.add_attributes (and Attrib.syntax);
authorwenzelm
Sat May 30 15:53:19 2009 +0200 (2009-05-30)
changeset 31306a74ee84288a0
parent 31305 a16f4d4f5b24
child 31307 7015fee8c3e8
eliminated old Attrib.add_attributes (and Attrib.syntax);
NEWS
src/Pure/Isar/attrib.ML
     1.1 --- a/NEWS	Sat May 30 15:25:46 2009 +0200
     1.2 +++ b/NEWS	Sat May 30 15:53:19 2009 +0200
     1.3 @@ -28,9 +28,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 -* Eliminated old Method.add_methods and related cominators for "method
     1.8 -args".  INCOMPATIBILITY, need to use simplified Method.setup
     1.9 -introduced in Isabelle2009.
    1.10 +* Eliminated old Attrib.add_attributes, Method.add_methods and related
    1.11 +cominators for "args".  INCOMPATIBILITY, need to use simplified
    1.12 +Attrib/Method.setup introduced in Isabelle2009.
    1.13  
    1.14  
    1.15  
     2.1 --- a/src/Pure/Isar/attrib.ML	Sat May 30 15:25:46 2009 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sat May 30 15:53:19 2009 +0200
     2.3 @@ -26,8 +26,6 @@
     2.4      (('c * 'a list) * ('b * 'a list) list) list ->
     2.5      (('c * 'att list) * ('fact * 'att list) list) list
     2.6    val crude_closure: Proof.context -> src -> src
     2.7 -  val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
     2.8 -  val syntax: attribute context_parser -> src -> attribute
     2.9    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    2.10    val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    2.11      theory -> theory
    2.12 @@ -87,6 +85,10 @@
    2.13      |> Pretty.chunks |> Pretty.writeln
    2.14    end;
    2.15  
    2.16 +fun add_attribute name att comment thy = thy |> Attributes.map (fn atts =>
    2.17 +  #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts)
    2.18 +    handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup));
    2.19 +
    2.20  
    2.21  (* name space *)
    2.22  
    2.23 @@ -147,24 +149,13 @@
    2.24    Args.closure src);
    2.25  
    2.26  
    2.27 -(* add_attributes *)
    2.28 -
    2.29 -fun add_attributes raw_attrs thy =
    2.30 -  let
    2.31 -    val new_attrs =
    2.32 -      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
    2.33 -    fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs
    2.34 -      handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
    2.35 -  in Attributes.map add thy end;
    2.36 -
    2.37 -
    2.38  (* attribute setup *)
    2.39  
    2.40 -fun syntax scan src (context, th) =
    2.41 -  let val (f: attribute, context') = Args.syntax "attribute" scan src context
    2.42 -  in f (context', th) end;
    2.43 +fun syntax scan = Args.syntax "attribute" scan;
    2.44  
    2.45 -fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
    2.46 +fun setup name scan =
    2.47 +  add_attribute name
    2.48 +    (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
    2.49  
    2.50  fun attribute_setup name (txt, pos) cmt =
    2.51    Context.theory_map (ML_Context.expression pos
    2.52 @@ -378,8 +369,8 @@
    2.53      val name = Sign.full_bname thy bname;
    2.54    in
    2.55      thy
    2.56 -    |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),
    2.57 -      "configuration option")]
    2.58 +    |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
    2.59 +      "configuration option"
    2.60      |> Configs.map (Symtab.update (name, config))
    2.61    end;
    2.62