apply_method/end_proof: pass position;
authorwenzelm
Wed Jun 13 00:02:03 2007 +0200 (2007-06-13)
changeset 233609e3c0c1ad0ad
parent 23359 6e1786a6f636
child 23361 df3d21caad2c
apply_method/end_proof: pass position;
Method.Basic: include position;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Jun 13 00:02:02 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jun 13 00:02:03 2007 +0200
     1.3 @@ -378,10 +378,11 @@
     1.4  fun goal_cases st =
     1.5    RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
     1.6  
     1.7 -fun apply_method current_context meth_fun state =
     1.8 +fun apply_method current_context pos meth_fun state =
     1.9    let
    1.10      val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
    1.11 -    val meth = meth_fun (if current_context then context_of state else goal_ctxt);
    1.12 +    val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt);
    1.13 +    val meth = meth_fun ctxt;
    1.14    in
    1.15      Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>
    1.16        state
    1.17 @@ -401,15 +402,16 @@
    1.18      |> Seq.maps meth
    1.19      |> Seq.maps (fn state' => state'
    1.20        |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
    1.21 -    |> Seq.maps (apply_method true (K Method.succeed)));
    1.22 +    |> Seq.maps (apply_method true Position.none (K Method.succeed)));
    1.23  
    1.24  fun apply_text cc text state =
    1.25    let
    1.26      val thy = theory_of state;
    1.27 +    val pos_of = #2 o Args.dest_src;
    1.28  
    1.29 -    fun eval (Method.Basic m) = apply_method cc m
    1.30 -      | eval (Method.Source src) = apply_method cc (Method.method thy src)
    1.31 -      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
    1.32 +    fun eval (Method.Basic (m, pos)) = apply_method cc pos m
    1.33 +      | eval (Method.Source src) = apply_method cc (pos_of src) (Method.method thy src)
    1.34 +      | eval (Method.Source_i src) = apply_method cc (pos_of src) (Method.method_i thy src)
    1.35        | eval (Method.Then txts) = Seq.EVERY (map eval txts)
    1.36        | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
    1.37        | eval (Method.Try txt) = Seq.TRY (eval txt)
    1.38 @@ -423,7 +425,7 @@
    1.39  val refine_end = apply_text false;
    1.40  
    1.41  fun refine_insert [] = I
    1.42 -  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
    1.43 +  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths), Position.none));
    1.44  
    1.45  end;
    1.46  
    1.47 @@ -708,20 +710,21 @@
    1.48    #> refine (the_default Method.default_text opt_text)
    1.49    #> Seq.map (using_facts [] #> enter_forward);
    1.50  
    1.51 -fun end_proof bot txt =
    1.52 -  assert_forward
    1.53 -  #> assert_bottom bot
    1.54 -  #> close_block
    1.55 -  #> assert_current_goal true
    1.56 -  #> using_facts []
    1.57 -  #> `before_qed #-> (refine o the_default Method.succeed_text)
    1.58 -  #> Seq.maps (refine (Method.finish_text txt));
    1.59 +fun end_proof bot txt state =
    1.60 +  state
    1.61 +  |> assert_forward
    1.62 +  |> assert_bottom bot
    1.63 +  |> close_block
    1.64 +  |> assert_current_goal true
    1.65 +  |> using_facts []
    1.66 +  |> `before_qed |-> (refine o the_default Method.succeed_text)
    1.67 +  |> Seq.maps (refine (Method.finish_text txt (ContextPosition.get (context_of state))));
    1.68  
    1.69  
    1.70  (* unstructured refinement *)
    1.71  
    1.72 -fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
    1.73 -fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
    1.74 +fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i), Position.none));
    1.75 +fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i), Position.none));
    1.76  
    1.77  fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
    1.78  fun apply_end text = assert_forward #> refine_end text;
    1.79 @@ -747,7 +750,7 @@
    1.80  fun refine_terms n =
    1.81    refine (Method.Basic (K (Method.RAW_METHOD
    1.82      (K (HEADGOAL (PRECISE_CONJUNCTS n
    1.83 -      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
    1.84 +      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
    1.85    #> Seq.hd;
    1.86  
    1.87  in
    1.88 @@ -785,7 +788,7 @@
    1.89      |> put_goal NONE
    1.90      |> enter_backward
    1.91      |> not (null vars) ? refine_terms (length propss')
    1.92 -    |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
    1.93 +    |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
    1.94    end;
    1.95  
    1.96  fun generic_qed state =