src/Pure/Isar/attrib.ML
changeset 31306 a74ee84288a0
parent 31305 a16f4d4f5b24
child 31323 89f218fcab2a
child 31358 3e640334a1b3
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat May 30 15:25:46 2009 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat May 30 15:53:19 2009 +0200
     1.3 @@ -26,8 +26,6 @@
     1.4      (('c * 'a list) * ('b * 'a list) list) list ->
     1.5      (('c * 'att list) * ('fact * 'att list) list) list
     1.6    val crude_closure: Proof.context -> src -> src
     1.7 -  val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
     1.8 -  val syntax: attribute context_parser -> src -> attribute
     1.9    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    1.10    val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    1.11      theory -> theory
    1.12 @@ -87,6 +85,10 @@
    1.13      |> Pretty.chunks |> Pretty.writeln
    1.14    end;
    1.15  
    1.16 +fun add_attribute name att comment thy = thy |> Attributes.map (fn atts =>
    1.17 +  #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts)
    1.18 +    handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup));
    1.19 +
    1.20  
    1.21  (* name space *)
    1.22  
    1.23 @@ -147,24 +149,13 @@
    1.24    Args.closure src);
    1.25  
    1.26  
    1.27 -(* add_attributes *)
    1.28 -
    1.29 -fun add_attributes raw_attrs thy =
    1.30 -  let
    1.31 -    val new_attrs =
    1.32 -      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
    1.33 -    fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs
    1.34 -      handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
    1.35 -  in Attributes.map add thy end;
    1.36 -
    1.37 -
    1.38  (* attribute setup *)
    1.39  
    1.40 -fun syntax scan src (context, th) =
    1.41 -  let val (f: attribute, context') = Args.syntax "attribute" scan src context
    1.42 -  in f (context', th) end;
    1.43 +fun syntax scan = Args.syntax "attribute" scan;
    1.44  
    1.45 -fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
    1.46 +fun setup name scan =
    1.47 +  add_attribute name
    1.48 +    (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
    1.49  
    1.50  fun attribute_setup name (txt, pos) cmt =
    1.51    Context.theory_map (ML_Context.expression pos
    1.52 @@ -378,8 +369,8 @@
    1.53      val name = Sign.full_bname thy bname;
    1.54    in
    1.55      thy
    1.56 -    |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),
    1.57 -      "configuration option")]
    1.58 +    |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
    1.59 +      "configuration option"
    1.60      |> Configs.map (Symtab.update (name, config))
    1.61    end;
    1.62