localized method definitions (see also f14c1248d064);

--- a/src/Pure/Isar/method.ML	Thu Aug 14 10:48:40 2014 +0200
+++ b/src/Pure/Isar/method.ML	Thu Aug 14 11:51:17 2014 +0200
@@ -66,7 +66,10 @@
   val check_name: Proof.context -> xstring * Position.T -> string
   val method: Proof.context -> src -> Proof.context -> method
   val method_cmd: Proof.context -> src -> Proof.context -> method
+  val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
+  val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
+    local_theory -> local_theory
   val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
@@ -309,7 +312,7 @@
 
 (* method definitions *)
 
-structure Methods = Theory_Data
+structure Methods = Generic_Data
 (
   type T = ((src -> Proof.context -> method) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "method";
@@ -317,7 +320,13 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-val get_methods = Methods.get o Proof_Context.theory_of;
+val get_methods = Methods.get o Context.Proof;
+
+fun transfer_methods thy ctxt =
+  let
+    val meths' =
+      Name_Space.merge_tables (Methods.get (Context.Theory thy), get_methods ctxt);
+  in Context.proof_map (Methods.put meths') ctxt end;
 
 fun print_methods ctxt =
   let
@@ -331,8 +340,34 @@
     |> Pretty.writeln_chunks
   end;
 
-fun add_method name meth comment thy = thy
-  |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
+
+(* define *)
+
+fun define_global binding meth comment thy =
+  let
+    val context = Context.Theory thy;
+    val (name, meths') =
+      Name_Space.define context true (binding, (meth, comment)) (Methods.get context);
+  in (name, Context.the_theory (Methods.put meths' context)) end;
+
+fun define binding meth comment lthy =
+  let
+    val standard_morphism =
+      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+    val meth0 = meth o Args.transform_values standard_morphism;
+  in
+    lthy
+    |> Local_Theory.background_theory_result (define_global binding meth0 comment)
+    |-> (fn name =>
+      Local_Theory.map_contexts
+        (fn _ => fn ctxt => transfer_methods (Proof_Context.theory_of ctxt) ctxt)
+      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+          let
+            val naming = Name_Space.naming_of context;
+            val binding' = Morphism.binding phi binding;
+          in Methods.map (Name_Space.alias_table naming binding' name) context end)
+      #> pair name)
+  end;
 
 
 (* check *)
@@ -360,9 +395,11 @@
 
 (* method setup *)
 
-fun setup name scan =
-  add_method name
-    (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
+fun method_syntax scan src ctxt : method =
+  let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end;
+
+fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
+fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
 
 fun method_setup name source cmt =
   Context.theory_map (ML_Context.expression (#pos source)