statement: keep explicit position;
authorwenzelm
Thu Jan 24 23:51:19 2008 +0100 (2008-01-24)
changeset 25958bcedde463850
parent 25957 2cfb703fa8d8
child 25959 9ad285dbc7a4
statement: keep explicit position;
replaced ContextPosition by Position.thread_data;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jan 24 23:51:18 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jan 24 23:51:19 2008 +0100
     1.3 @@ -137,10 +137,11 @@
     1.4      goal: goal option}
     1.5  and goal =
     1.6    Goal of
     1.7 -   {statement: string * term list list,     (*goal kind and statement, starting with vars*)
     1.8 -    messages: (unit -> Pretty.T) list,      (*persistent messages (hints etc.)*)
     1.9 -    using: thm list,                        (*goal facts*)
    1.10 -    goal: thm,                              (*subgoals ==> statement*)
    1.11 +   {statement: (string * Position.T) * term list list,
    1.12 +                                          (*goal kind and statement (starting with vars)*)
    1.13 +    messages: (unit -> Pretty.T) list,    (*persistent messages (hints etc.)*)
    1.14 +    using: thm list,                      (*goal facts*)
    1.15 +    goal: thm,                            (*subgoals ==> statement*)
    1.16      before_qed: Method.text option,
    1.17      after_qed:
    1.18        (thm list list -> state -> state Seq.seq) *
    1.19 @@ -340,14 +341,14 @@
    1.20        | strs' => enclose " (" ")" (commas strs'));
    1.21  
    1.22      fun prt_goal (SOME (ctxt, (i,
    1.23 -            {statement = _, messages, using, goal, before_qed, after_qed}))) =
    1.24 +            {statement = ((_, pos), _), messages, using, goal, before_qed, after_qed}))) =
    1.25            pretty_facts "using " ctxt
    1.26              (if mode <> Backward orelse null using then NONE else SOME using) @
    1.27            [Pretty.str ("goal" ^
    1.28              description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
    1.29            pretty_goals_local ctxt Markup.subgoal
    1.30              (true, ! show_main_goal) (! Display.goals_limit) goal @
    1.31 -          (map (fn msg => msg ()) (rev messages))
    1.32 +          (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
    1.33        | prt_goal NONE = [];
    1.34  
    1.35      val prt_ctxt =
    1.36 @@ -385,15 +386,13 @@
    1.37  fun goal_cases st =
    1.38    RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
    1.39  
    1.40 -fun apply_method current_context pos meth_fun state =
    1.41 +fun apply_method current_context pos meth state =
    1.42    let
    1.43      val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
    1.44        find_goal state;
    1.45 -    val ctxt = ContextPosition.put_ctxt pos
    1.46 -      (if current_context then context_of state else goal_ctxt);
    1.47 -    val meth = meth_fun ctxt;
    1.48 +    val ctxt = if current_context then context_of state else goal_ctxt;
    1.49    in
    1.50 -    Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>
    1.51 +    Method.apply pos meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    1.52        state
    1.53        |> map_goal
    1.54            (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
    1.55 @@ -743,7 +742,7 @@
    1.56    |> assert_current_goal true
    1.57    |> using_facts []
    1.58    |> `before_qed |-> (refine o the_default Method.succeed_text)
    1.59 -  |> Seq.maps (refine (Method.finish_text txt (ContextPosition.get (context_of state))));
    1.60 +  |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
    1.61  
    1.62  
    1.63  (* unstructured refinement *)
    1.64 @@ -785,6 +784,7 @@
    1.65      val thy = theory_of state;
    1.66      val cert = Thm.cterm_of thy;
    1.67      val chaining = can assert_chain state;
    1.68 +    val pos = Position.thread_data ();
    1.69  
    1.70      val ((propss, after_ctxt), goal_state) =
    1.71        state
    1.72 @@ -807,7 +807,7 @@
    1.73    in
    1.74      goal_state
    1.75      |> map_context (init_context #> Variable.set_body true)
    1.76 -    |> put_goal (SOME (make_goal ((kind, propss'), [], [], goal, before_qed, after_qed')))
    1.77 +    |> put_goal (SOME (make_goal (((kind, pos), propss'), [], [], goal, before_qed, after_qed')))
    1.78      |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
    1.79      |> map_context (ProofContext.auto_bind_goal props)
    1.80      |> chaining ? (`the_facts #-> using_facts)
    1.81 @@ -821,20 +821,25 @@
    1.82  
    1.83  fun generic_qed state =
    1.84    let
    1.85 -    val (goal_ctxt, {statement = (_, stmt), goal, after_qed, ...}) = current_goal state;
    1.86 +    val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state;
    1.87      val outer_state = state |> close_block;
    1.88      val outer_ctxt = context_of outer_state;
    1.89  
    1.90 +    val ((_, pos), stmt) = statement;
    1.91      val props =
    1.92        flat (tl stmt)
    1.93        |> Variable.exportT_terms goal_ctxt outer_ctxt;
    1.94      val results =
    1.95        tl (conclude_goal state goal stmt)
    1.96        |> burrow (ProofContext.export goal_ctxt outer_ctxt);
    1.97 +
    1.98 +    val (after_local, after_global) = after_qed;
    1.99 +    fun after_local' x y = Position.setmp_thread_data_seq pos (fn () => after_local x y) ();
   1.100 +    fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
   1.101    in
   1.102      outer_state
   1.103      |> map_context (ProofContext.auto_bind_facts props)
   1.104 -    |> pair (after_qed, results)
   1.105 +    |> pair ((after_local', after_global'), results)
   1.106    end;
   1.107  
   1.108  end;