# HG changeset patch
# User wenzelm
# Date 1465307058 -7200
# Node ID 96cfb07c60d4c4bbb445815391a2a7f5d74ac356
# Parent  d1693d7b0c01dd8b886cf723596dfa41269b9966
expode method_facts via dynamic method context;

diff -r d1693d7b0c01 -r 96cfb07c60d4 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Jun 07 11:27:01 2016 +0200
+++ b/src/Pure/Isar/method.ML	Tue Jun 07 15:44:18 2016 +0200
@@ -54,6 +54,8 @@
   val drule: Proof.context -> int -> thm list -> method
   val frule: Proof.context -> int -> thm list -> method
   val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
+  val get_facts: Proof.context -> thm list
+  val map_facts: (thm list -> thm list) -> Proof.context -> Proof.context
   type combinator_info
   val no_combinator_info: combinator_info
   datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int
@@ -322,26 +324,37 @@
 structure Data = Generic_Data
 (
   type T =
-    ((Token.src -> Proof.context -> method) * string) Name_Space.table *  (*methods*)
-    (morphism -> thm list -> tactic) option;  (*ML tactic*)
-  val empty : T = (Name_Space.empty_table "method", NONE);
+   {methods: ((Token.src -> Proof.context -> method) * string) Name_Space.table,
+    ml_tactic: (morphism -> thm list -> tactic) option,
+    facts: thm list option};
+  val empty : T =
+    {methods = Name_Space.empty_table "method", ml_tactic = NONE, facts = NONE};
   val extend = I;
-  fun merge ((tab, tac), (tab', tac')) : T =
-    (Name_Space.merge_tables (tab, tab'), merge_options (tac, tac'));
+  fun merge
+    ({methods = methods1, ml_tactic = ml_tactic1, facts = facts1},
+     {methods = methods2, ml_tactic = ml_tactic2, facts = facts2}) : T =
+    {methods = Name_Space.merge_tables (methods1, methods2),
+     ml_tactic = merge_options (ml_tactic1, ml_tactic2),
+     facts = merge_options (facts1, facts2)};
 );
 
-val get_methods = fst o Data.get;
-val map_methods = Data.map o apfst;
+fun map_data f = Data.map (fn {methods, ml_tactic, facts} =>
+  let val (methods', ml_tactic', facts') = f (methods, ml_tactic, facts)
+  in {methods = methods', ml_tactic = ml_tactic', facts = facts'} end);
 
-val ops_methods = {get_data = get_methods, put_data = map_methods o K};
+val get_methods = #methods o Data.get;
+
+val ops_methods =
+ {get_data = get_methods,
+  put_data = fn methods => map_data (fn (_, ml_tactic, facts) => (methods, ml_tactic, facts))};
 
 
 (* ML tactic *)
 
-val set_tactic = Data.map o apsnd o K o SOME;
+fun set_tactic ml_tactic = map_data (fn (methods, _, facts) => (methods, SOME ml_tactic, facts));
 
 fun the_tactic context =
-  (case snd (Data.get context) of
+  (case #ml_tactic (Data.get context) of
     SOME tac => tac
   | NONE => raise Fail "Undefined ML tactic");
 
@@ -361,6 +374,20 @@
       end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
 
 
+(* method facts *)
+
+val get_facts_generic = these o #facts o Data.get;
+val get_facts = get_facts_generic o Context.Proof;
+
+fun map_facts f =
+  (Context.proof_map o map_data)
+    (fn (methods, ml_tactic, facts) => (methods, ml_tactic, SOME (f (these facts))));
+
+val _ =
+  Theory.setup
+    (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", @{here}), get_facts_generic));
+
+
 (* method text *)
 
 datatype combinator_info = Combinator_Info of {keywords: Position.T list};
@@ -535,18 +562,15 @@
 
 in
 
-fun evaluate text ctxt =
+fun evaluate text static_ctxt =
   let
-    fun eval0 m facts = Seq.single #> Seq.maps_results (m facts);
-    fun eval (Basic m) = eval0 (m ctxt)
-      | eval (Source src) = eval0 (method_cmd ctxt src ctxt)
-      | eval (Combinator (_, c, txts)) =
-          let
-            val comb = combinator c;
-            val meths = map eval txts;
-          in fn facts => comb (map (fn meth => meth facts) meths) end;
-    val meth = eval text;
-  in fn facts => fn ctxt_st => meth facts (Seq.Result ctxt_st) end;
+    fun eval0 m =
+      Seq.single #> Seq.maps_results (fn (ctxt, st) => m (get_facts ctxt) (ctxt, st));
+    fun eval (Basic m) = eval0 (m static_ctxt)
+      | eval (Source src) = eval0 (method_cmd static_ctxt src static_ctxt)
+      | eval (Combinator (_, c, txts)) = combinator c (map eval txts);
+    val method = eval text;
+  in fn facts => fn (ctxt, st) => method (Seq.Result (map_facts (K facts) ctxt, st)) end;
 
 end;