localized method definitions (see also f14c1248d064);
authorwenzelm
Thu Aug 14 11:51:17 2014 +0200 (2014-08-14)
changeset 57935c578f3a37a67
parent 57934 5e500c0e7eca
child 57936 74ea9ba645c3
localized method definitions (see also f14c1248d064);
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Thu Aug 14 10:48:40 2014 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Aug 14 11:51:17 2014 +0200
     1.3 @@ -66,7 +66,10 @@
     1.4    val check_name: Proof.context -> xstring * Position.T -> string
     1.5    val method: Proof.context -> src -> Proof.context -> method
     1.6    val method_cmd: Proof.context -> src -> Proof.context -> method
     1.7 +  val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
     1.8    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
     1.9 +  val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
    1.10 +    local_theory -> local_theory
    1.11    val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
    1.12    type modifier = (Proof.context -> Proof.context) * attribute
    1.13    val section: modifier parser list -> thm list context_parser
    1.14 @@ -309,7 +312,7 @@
    1.15  
    1.16  (* method definitions *)
    1.17  
    1.18 -structure Methods = Theory_Data
    1.19 +structure Methods = Generic_Data
    1.20  (
    1.21    type T = ((src -> Proof.context -> method) * string) Name_Space.table;
    1.22    val empty : T = Name_Space.empty_table "method";
    1.23 @@ -317,7 +320,13 @@
    1.24    fun merge data : T = Name_Space.merge_tables data;
    1.25  );
    1.26  
    1.27 -val get_methods = Methods.get o Proof_Context.theory_of;
    1.28 +val get_methods = Methods.get o Context.Proof;
    1.29 +
    1.30 +fun transfer_methods thy ctxt =
    1.31 +  let
    1.32 +    val meths' =
    1.33 +      Name_Space.merge_tables (Methods.get (Context.Theory thy), get_methods ctxt);
    1.34 +  in Context.proof_map (Methods.put meths') ctxt end;
    1.35  
    1.36  fun print_methods ctxt =
    1.37    let
    1.38 @@ -331,8 +340,34 @@
    1.39      |> Pretty.writeln_chunks
    1.40    end;
    1.41  
    1.42 -fun add_method name meth comment thy = thy
    1.43 -  |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
    1.44 +
    1.45 +(* define *)
    1.46 +
    1.47 +fun define_global binding meth comment thy =
    1.48 +  let
    1.49 +    val context = Context.Theory thy;
    1.50 +    val (name, meths') =
    1.51 +      Name_Space.define context true (binding, (meth, comment)) (Methods.get context);
    1.52 +  in (name, Context.the_theory (Methods.put meths' context)) end;
    1.53 +
    1.54 +fun define binding meth comment lthy =
    1.55 +  let
    1.56 +    val standard_morphism =
    1.57 +      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    1.58 +    val meth0 = meth o Args.transform_values standard_morphism;
    1.59 +  in
    1.60 +    lthy
    1.61 +    |> Local_Theory.background_theory_result (define_global binding meth0 comment)
    1.62 +    |-> (fn name =>
    1.63 +      Local_Theory.map_contexts
    1.64 +        (fn _ => fn ctxt => transfer_methods (Proof_Context.theory_of ctxt) ctxt)
    1.65 +      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    1.66 +          let
    1.67 +            val naming = Name_Space.naming_of context;
    1.68 +            val binding' = Morphism.binding phi binding;
    1.69 +          in Methods.map (Name_Space.alias_table naming binding' name) context end)
    1.70 +      #> pair name)
    1.71 +  end;
    1.72  
    1.73  
    1.74  (* check *)
    1.75 @@ -360,9 +395,11 @@
    1.76  
    1.77  (* method setup *)
    1.78  
    1.79 -fun setup name scan =
    1.80 -  add_method name
    1.81 -    (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
    1.82 +fun method_syntax scan src ctxt : method =
    1.83 +  let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
    1.84 +
    1.85 +fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
    1.86 +fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
    1.87  
    1.88  fun method_setup name source cmt =
    1.89    Context.theory_map (ML_Context.expression (#pos source)