src/Tools/Code/code_preproc.ML
changeset 31998 2c7a24f74db9
parent 31977 e03059ae2d82
child 32072 d4bff63bcbf1
     1.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -526,14 +526,16 @@
     1.4  val setup = 
     1.5    let
     1.6      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     1.7 -    fun add_del_attribute (name, (add, del)) =
     1.8 -      Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
     1.9 -        || Scan.succeed (mk_attribute add))
    1.10 +    fun add_del_attribute_parser (add, del) =
    1.11 +      Attrib.add_del (mk_attribute add) (mk_attribute del);
    1.12    in
    1.13 -    add_del_attribute ("inline", (add_inline, del_inline))
    1.14 -    #> add_del_attribute ("post", (add_post, del_post))
    1.15 -    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
    1.16 -       (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
    1.17 +    Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
    1.18 +        "preprocessing equations for code generator"
    1.19 +    #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
    1.20 +        "postprocessing equations for code generator"
    1.21 +    #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
    1.22 +       (fn thm => Codegen.add_unfold thm #> add_inline thm)))
    1.23 +        "preprocessing equations for code generators"
    1.24    end;
    1.25  
    1.26  val _ =