src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Wed Jun 13 00:02:02 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 13 00:02:03 2007 +0200
@@ -378,10 +378,11 @@
 fun goal_cases st =
   RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
-fun apply_method current_context meth_fun state =
+fun apply_method current_context pos meth_fun state =
   let
     val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
-    val meth = meth_fun (if current_context then context_of state else goal_ctxt);
+    val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt);
+    val meth = meth_fun ctxt;
   in
     Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>
       state
@@ -401,15 +402,16 @@
     |> Seq.maps meth
     |> Seq.maps (fn state' => state'
       |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
-    |> Seq.maps (apply_method true (K Method.succeed)));
+    |> Seq.maps (apply_method true Position.none (K Method.succeed)));
 
 fun apply_text cc text state =
   let
     val thy = theory_of state;
+    val pos_of = #2 o Args.dest_src;
 
-    fun eval (Method.Basic m) = apply_method cc m
-      | eval (Method.Source src) = apply_method cc (Method.method thy src)
-      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
+    fun eval (Method.Basic (m, pos)) = apply_method cc pos m
+      | eval (Method.Source src) = apply_method cc (pos_of src) (Method.method thy src)
+      | eval (Method.Source_i src) = apply_method cc (pos_of src) (Method.method_i thy src)
       | eval (Method.Then txts) = Seq.EVERY (map eval txts)
       | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
       | eval (Method.Try txt) = Seq.TRY (eval txt)
@@ -423,7 +425,7 @@
 val refine_end = apply_text false;
 
 fun refine_insert [] = I
-  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths), Position.none));
 
 end;
 
@@ -708,20 +710,21 @@
   #> refine (the_default Method.default_text opt_text)
   #> Seq.map (using_facts [] #> enter_forward);
 
-fun end_proof bot txt =
-  assert_forward
-  #> assert_bottom bot
-  #> close_block
-  #> assert_current_goal true
-  #> using_facts []
-  #> `before_qed #-> (refine o the_default Method.succeed_text)
-  #> Seq.maps (refine (Method.finish_text txt));
+fun end_proof bot txt state =
+  state
+  |> assert_forward
+  |> assert_bottom bot
+  |> close_block
+  |> assert_current_goal true
+  |> using_facts []
+  |> `before_qed |-> (refine o the_default Method.succeed_text)
+  |> Seq.maps (refine (Method.finish_text txt (ContextPosition.get (context_of state))));
 
 
 (* unstructured refinement *)
 
-fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
-fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
+fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i), Position.none));
+fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i), Position.none));
 
 fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
 fun apply_end text = assert_forward #> refine_end text;
@@ -747,7 +750,7 @@
 fun refine_terms n =
   refine (Method.Basic (K (Method.RAW_METHOD
     (K (HEADGOAL (PRECISE_CONJUNCTS n
-      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
+      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
   #> Seq.hd;
 
 in
@@ -785,7 +788,7 @@
     |> put_goal NONE
     |> enter_backward
     |> not (null vars) ? refine_terms (length propss')
-    |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+    |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
   end;
 
 fun generic_qed state =