localized attribute definitions;
authorwenzelm
Wed Aug 13 13:57:55 2014 +0200 (2014-08-13)
changeset 57927f14c1248d064
parent 57926 59b2572e8e93
child 57928 f4ff42c5b05b
localized attribute definitions;
src/Pure/Isar/attrib.ML
src/Pure/Tools/named_theorems.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Wed Aug 13 13:30:28 2014 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Aug 13 13:57:55 2014 +0200
     1.3 @@ -11,6 +11,10 @@
     1.4    val empty_binding: binding
     1.5    val is_empty_binding: binding -> bool
     1.6    val print_attributes: Proof.context -> unit
     1.7 +  val define_global: Binding.binding -> (Args.src -> attribute) ->
     1.8 +    string -> theory -> string * theory
     1.9 +  val define: Binding.binding -> (Args.src -> attribute) ->
    1.10 +    string -> local_theory -> string * local_theory
    1.11    val check_name_generic: Context.generic -> xstring * Position.T -> string
    1.12    val check_name: Proof.context -> xstring * Position.T -> string
    1.13    val check_src: Proof.context -> src -> src
    1.14 @@ -35,6 +39,8 @@
    1.15      Context.generic -> (string * thm list) list * Context.generic
    1.16    val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
    1.17    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    1.18 +  val local_setup: Binding.binding -> attribute context_parser -> string ->
    1.19 +    local_theory -> local_theory
    1.20    val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    1.21    val internal: (morphism -> attribute) -> src
    1.22    val add_del: attribute -> attribute -> attribute context_parser
    1.23 @@ -74,7 +80,6 @@
    1.24  (* source and bindings *)
    1.25  
    1.26  type src = Args.src;
    1.27 -
    1.28  type binding = binding * src list;
    1.29  
    1.30  val empty_binding: binding = (Binding.empty, []);
    1.31 @@ -86,7 +91,7 @@
    1.32  
    1.33  (* theory data *)
    1.34  
    1.35 -structure Attributes = Theory_Data
    1.36 +structure Attributes = Generic_Data
    1.37  (
    1.38    type T = ((src -> attribute) * string) Name_Space.table;
    1.39    val empty : T = Name_Space.empty_table "attribute";
    1.40 @@ -94,11 +99,17 @@
    1.41    fun merge data : T = Name_Space.merge_tables data;
    1.42  );
    1.43  
    1.44 -val get_attributes = Attributes.get o Context.theory_of;
    1.45 +val get_attributes = Attributes.get o Context.Proof;
    1.46 +
    1.47 +fun transfer_attributes thy ctxt =
    1.48 +  let
    1.49 +    val attribs' =
    1.50 +      Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt);
    1.51 +  in Context.proof_map (Attributes.put attribs') ctxt end;
    1.52  
    1.53  fun print_attributes ctxt =
    1.54    let
    1.55 -    val attribs = get_attributes (Context.Proof ctxt);
    1.56 +    val attribs = get_attributes ctxt;
    1.57      fun prt_attr (name, (_, "")) = Pretty.mark_str name
    1.58        | prt_attr (name, (_, comment)) =
    1.59            Pretty.block
    1.60 @@ -108,20 +119,46 @@
    1.61      |> Pretty.writeln_chunks
    1.62    end;
    1.63  
    1.64 -val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof;
    1.65 +val attribute_space = Name_Space.space_of_table o get_attributes;
    1.66 +
    1.67 +
    1.68 +(* define *)
    1.69 +
    1.70 +fun define_global binding att comment thy =
    1.71 +  let
    1.72 +    val context = Context.Theory thy;
    1.73 +    val (name, attribs') =
    1.74 +      Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
    1.75 +  in (name, Context.the_theory (Attributes.put attribs' context)) end;
    1.76  
    1.77 -fun add_attribute name att comment thy = thy
    1.78 -  |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
    1.79 +fun define binding att comment lthy =
    1.80 +  let
    1.81 +    val standard_morphism =
    1.82 +      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    1.83 +    val att0 = att o Args.transform_values standard_morphism;
    1.84 +  in
    1.85 +    lthy
    1.86 +    |> Local_Theory.background_theory_result (define_global binding att0 comment)
    1.87 +    |-> (fn name =>
    1.88 +      Local_Theory.map_contexts
    1.89 +        (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt)
    1.90 +      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    1.91 +          let
    1.92 +            val naming = Name_Space.naming_of context;
    1.93 +            val binding' = Morphism.binding phi binding;
    1.94 +          in Attributes.map (Name_Space.alias_table naming binding' name) context end)
    1.95 +      #> pair name)
    1.96 +  end;
    1.97  
    1.98  
    1.99  (* check *)
   1.100  
   1.101 -fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
   1.102 +fun check_name_generic context = #1 o Name_Space.check context (Attributes.get context);
   1.103  val check_name = check_name_generic o Context.Proof;
   1.104  
   1.105  fun check_src ctxt src =
   1.106   (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
   1.107 -  #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src));
   1.108 +  #1 (Args.check_src ctxt (get_attributes ctxt) src));
   1.109  
   1.110  
   1.111  (* pretty printing *)
   1.112 @@ -133,7 +170,7 @@
   1.113  (* get attributes *)
   1.114  
   1.115  fun attribute_generic context =
   1.116 -  let val table = get_attributes context
   1.117 +  let val table = Attributes.get context
   1.118    in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
   1.119  
   1.120  val attribute = attribute_generic o Context.Proof;
   1.121 @@ -171,10 +208,11 @@
   1.122  
   1.123  (* attribute setup *)
   1.124  
   1.125 -fun setup name scan =
   1.126 -  add_attribute name
   1.127 -    (fn src => fn (ctxt, th) =>
   1.128 -      let val (a, ctxt') = Args.syntax_generic scan src ctxt in a (ctxt', th) end);
   1.129 +fun attribute_syntax scan src (context, th) =
   1.130 +  let val (a, context') = Args.syntax_generic scan src context in a (context', th) end;
   1.131 +
   1.132 +fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
   1.133 +fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
   1.134  
   1.135  fun attribute_setup name source cmt =
   1.136    Context.theory_map (ML_Context.expression (#pos source)
     2.1 --- a/src/Pure/Tools/named_theorems.ML	Wed Aug 13 13:30:28 2014 +0200
     2.2 +++ b/src/Pure/Tools/named_theorems.ML	Wed Aug 13 13:57:55 2014 +0200
     2.3 @@ -67,9 +67,9 @@
     2.4      val lthy' = lthy
     2.5        |> Local_Theory.background_theory
     2.6          (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #>
     2.7 -         Attrib.setup binding (Attrib.add_del (add name) (del name)) description #>
     2.8           Context.theory_map (new_entry name))
     2.9        |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
    2.10 +      |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
    2.11        |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
    2.12            let
    2.13              val binding' = Morphism.binding phi binding;