--- 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)