src/Pure/Isar/attrib.ML
changeset 47815 43f677b3ae91
parent 47249 c0481c3c2a6c
child 47816 cd0dfb06b0c8
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Apr 27 21:47:47 2012 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Apr 27 22:47:30 2012 +0200
     1.3 @@ -15,8 +15,10 @@
     1.4    val intern_src: theory -> src -> src
     1.5    val pretty_attribs: Proof.context -> src list -> Pretty.T list
     1.6    val defined: theory -> string -> bool
     1.7 -  val attribute: theory -> src -> attribute
     1.8 -  val attribute_i: theory -> src -> attribute
     1.9 +  val attribute: Proof.context -> src -> attribute
    1.10 +  val attribute_global: theory -> src -> attribute
    1.11 +  val attribute_cmd: Proof.context -> src -> attribute
    1.12 +  val attribute_cmd_global: theory -> src -> attribute
    1.13    val map_specs: ('a list -> 'att list) ->
    1.14      (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
    1.15    val map_facts: ('a list -> 'att list) ->
    1.16 @@ -120,7 +122,7 @@
    1.17  
    1.18  val defined = Symtab.defined o #2 o Attributes.get;
    1.19  
    1.20 -fun attribute_i thy =
    1.21 +fun attribute_global thy =
    1.22    let
    1.23      val (space, tab) = Attributes.get thy;
    1.24      fun attr src =
    1.25 @@ -131,7 +133,11 @@
    1.26        end;
    1.27    in attr end;
    1.28  
    1.29 -fun attribute thy = attribute_i thy o intern_src thy;
    1.30 +val attribute = attribute_global o Proof_Context.theory_of;
    1.31 +val attribute_generic = attribute_global o Context.theory_of;
    1.32 +
    1.33 +fun attribute_cmd_global thy = attribute_global thy o intern_src thy;
    1.34 +val attribute_cmd = attribute_cmd_global o Proof_Context.theory_of;
    1.35  
    1.36  
    1.37  (* attributed declarations *)
    1.38 @@ -145,17 +151,17 @@
    1.39  (* fact expressions *)
    1.40  
    1.41  fun global_notes kind facts thy = thy |>
    1.42 -  Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
    1.43 +  Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
    1.44  
    1.45  fun local_notes kind facts ctxt = ctxt |>
    1.46 -  Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
    1.47 +  Proof_Context.note_thmss kind (map_facts (map (attribute ctxt)) facts);
    1.48  
    1.49  fun generic_notes kind facts context = context |>
    1.50    Context.mapping_result (global_notes kind facts) (local_notes kind facts);
    1.51  
    1.52  fun eval_thms ctxt srcs = ctxt
    1.53    |> Proof_Context.note_thmss ""
    1.54 -    (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)
    1.55 +    (map_facts_refs (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt)
    1.56        [((Binding.empty, []), srcs)])
    1.57    |> fst |> maps snd;
    1.58  
    1.59 @@ -203,7 +209,7 @@
    1.60    in
    1.61      Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
    1.62        let
    1.63 -        val atts = map (attribute_i thy) srcs;
    1.64 +        val atts = map (attribute_generic context) srcs;
    1.65          val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
    1.66        in (context', pick "" [th']) end)
    1.67      ||
    1.68 @@ -215,7 +221,7 @@
    1.69      -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    1.70        let
    1.71          val ths = Facts.select thmref fact;
    1.72 -        val atts = map (attribute_i thy) srcs;
    1.73 +        val atts = map (attribute_generic context) srcs;
    1.74          val (ths', context') =
    1.75            fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
    1.76        in (context', pick name ths') end)
    1.77 @@ -240,7 +246,7 @@
    1.78  fun apply_att src (context, th) =
    1.79    let
    1.80      val src1 = Args.assignable src;
    1.81 -    val result = attribute_i (Context.theory_of context) src1 (context, th);
    1.82 +    val result = attribute_generic context src1 (context, th);
    1.83      val src2 = Args.closure src1;
    1.84    in (src2, result) end;
    1.85