modernized setup
authorhaftmann
Thu May 15 16:38:29 2014 +0200 (2014-05-15)
changeset 56970a3f911785efa
parent 56969 7491932da574
child 56971 f4942eb3bb03
modernized setup
src/Tools/Code/code_preproc.ML
src/Tools/Code_Generator.thy
     1.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:29 2014 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:29 2014 +0200
     1.3 @@ -32,8 +32,6 @@
     1.4    val static_value: Proof.context -> ((term -> term) -> 'a -> 'b) -> string list
     1.5      -> (code_algebra -> code_graph -> Proof.context -> term -> 'a)
     1.6      -> Proof.context -> term -> 'b
     1.7 -
     1.8 -  val setup: theory -> theory
     1.9  end
    1.10  
    1.11  structure Code_Preproc : CODE_PREPROC =
    1.12 @@ -507,19 +505,20 @@
    1.13  
    1.14  (** setup **)
    1.15  
    1.16 -val setup = 
    1.17 +val _ =
    1.18    let
    1.19      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    1.20      fun add_del_attribute_parser process =
    1.21        Attrib.add_del (mk_attribute (process Simplifier.add_simp))
    1.22          (mk_attribute (process Simplifier.del_simp));
    1.23    in
    1.24 -    Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
    1.25 +    Context.>> (Context.map_theory
    1.26 +      (Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
    1.27          "preprocessing equations for code generator"
    1.28 -    #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
    1.29 +      #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
    1.30          "postprocessing equations for code generator"
    1.31 -    #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
    1.32 -        "post- and preprocessing equations for code generator"
    1.33 +      #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
    1.34 +        "post- and preprocessing equations for code generator"))
    1.35    end;
    1.36  
    1.37  val _ =
     2.1 --- a/src/Tools/Code_Generator.thy	Thu May 15 16:38:29 2014 +0200
     2.2 +++ b/src/Tools/Code_Generator.thy	Thu May 15 16:38:29 2014 +0200
     2.3 @@ -27,8 +27,7 @@
     2.4  ML_file "~~/src/Tools/Code/code_scala.ML"
     2.5  
     2.6  setup {*
     2.7 -  Code_Preproc.setup
     2.8 -  #> Code_Simp.setup
     2.9 +  Code_Simp.setup
    2.10    #> Code_Target.setup
    2.11    #> Code_ML.setup
    2.12    #> Code_Haskell.setup