more method position information, notably finished_pos after end of previous text;

--- a/src/HOL/Statespace/state_space.ML	Wed Oct 17 10:46:14 2012 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Oct 17 13:20:08 2012 +0200
@@ -146,7 +146,7 @@
    thy
    |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
-         ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.none), NONE)
+         ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    |> Proof_Context.theory_of
 
 fun add_locale name expr elems thy =

--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 17 10:46:14 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 17 13:20:08 2012 +0200
@@ -30,8 +30,8 @@
   val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val qed: Method.text_position option -> Toplevel.transition -> Toplevel.transition
-  val terminal_proof: Method.text_position * Method.text_position option ->
+  val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
+  val terminal_proof: Method.text_range * Method.text_range option ->
     Toplevel.transition -> Toplevel.transition
   val default_proof: Toplevel.transition -> Toplevel.transition
   val immediate_proof: Toplevel.transition -> Toplevel.transition

--- a/src/Pure/Isar/method.ML	Wed Oct 17 10:46:14 2012 +0200
+++ b/src/Pure/Isar/method.ML	Wed Oct 17 13:20:08 2012 +0200
@@ -73,10 +73,10 @@
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
-  type text_position = text * Position.T
-  val parse: text_position parser
-  val text: text_position option -> text option
-  val position: text_position option -> Position.T
+  type text_range = text * Position.range
+  val parse: text_range parser
+  val text: text_range option -> text option
+  val position: text_range option -> Position.T
 end;
 
 structure Method: METHOD =
@@ -417,20 +417,20 @@
 in
 
 val parse =
-  Scan.trace meth3 >> (fn (m, toks) => (m, Position.set_range (Token.position_range_of toks)));
+  Scan.trace meth3 >> (fn (m, toks) => (m, Token.position_range_of toks));
 
 end;
 
 
 (* text position *)
 
-type text_position = text * Position.T;
+type text_range = text * Position.range;
 
 fun text NONE = NONE
   | text (SOME (txt, _)) = SOME txt;
 
 fun position NONE = Position.none
-  | position (SOME (_, pos)) = pos;
+  | position (SOME (_, range)) = Position.set_range range;
 
 
 (* theory setup *)

--- a/src/Pure/Isar/proof.ML	Wed Oct 17 10:46:14 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Oct 17 13:20:08 2012 +0200
@@ -77,30 +77,30 @@
   val begin_notepad: context -> state
   val end_notepad: state -> context
   val proof: Method.text option -> state -> state Seq.seq
-  val proof_results: Method.text_position option -> state -> state Seq.result Seq.seq
+  val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
   val defer: int -> state -> state
   val prefer: int -> state -> state
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq
-  val apply_results: Method.text_position -> state -> state Seq.result Seq.seq
-  val apply_end_results: Method.text_position -> state -> state Seq.result Seq.seq
+  val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
+  val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (context -> 'a -> attribute) ->
     ('b list -> context -> (term list list * (context -> context)) * context) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
     ((binding * 'a list) * 'b) list -> state -> state
-  val local_qed: Method.text_position option * bool -> state -> state
+  val local_qed: Method.text_range option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
   val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
-  val global_qed: Method.text_position option * bool -> state -> context
-  val local_terminal_proof: Method.text_position * Method.text_position option -> state -> state
+  val global_qed: Method.text_range option * bool -> state -> context
+  val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
   val local_default_proof: state -> state
   val local_immediate_proof: state -> state
   val local_skip_proof: bool -> state -> state
   val local_done_proof: state -> state
-  val global_terminal_proof: Method.text_position * Method.text_position option -> state -> context
+  val global_terminal_proof: Method.text_range * Method.text_range option -> state -> context
   val global_default_proof: state -> context
   val global_immediate_proof: state -> context
   val global_skip_proof: bool -> state -> context
@@ -116,9 +116,9 @@
   val schematic_goal: state -> bool
   val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
   val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
-  val local_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
+  val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
     state -> state
-  val global_future_terminal_proof: Method.text_position * Method.text_position option -> bool ->
+  val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
     state -> context
 end;
 
@@ -508,10 +508,13 @@
 
 val finished_goal_error = "Failed to finish proof";
 
-fun finished_goal state =
+fun finished_goal pos state =
   let val (ctxt, (_, goal)) = get_goal state in
     if Thm.no_prems goal then Seq.Result state
-    else Seq.Error (fn () => finished_goal_error ^ ":\n" ^ Proof_Display.string_of_goal ctxt goal)
+    else
+      Seq.Error (fn () =>
+        finished_goal_error ^ Position.here pos ^ ":\n" ^
+          Proof_Display.string_of_goal ctxt goal)
   end;
 
 
@@ -817,18 +820,25 @@
   Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
     method_error "initial" (Method.position arg));
 
-fun end_proof bot (arg, immed) =
-  Seq.APPEND (fn 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 (Method.text arg, immed)))
-    |> Seq.make_results, method_error "terminal" (Method.position arg))
-  #> Seq.maps_results (Seq.single o finished_goal);
+fun end_proof bot (prev_pos, (opt_text, immed)) =
+  let
+    val (finish_text, terminal_pos, finished_pos) =
+      (case opt_text of
+        NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
+      | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
+  in
+    Seq.APPEND (fn 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 finish_text)
+      |> Seq.make_results, method_error "terminal" terminal_pos)
+    #> Seq.maps_results (Seq.single o finished_goal finished_pos)
+  end;
 
 fun check_result msg sq =
   (case Seq.pull sq of
@@ -850,11 +860,11 @@
 
 fun apply_end text = assert_forward #> refine_end text;
 
-fun apply_results (text, pos) =
-  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
+fun apply_results (text, range) =
+  Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range));
 
-fun apply_end_results (text, pos) =
-  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
+fun apply_end_results (text, range) =
+  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" (Position.set_range range));
 
 
 
@@ -964,7 +974,8 @@
   #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
     (fn ((after_qed, _), results) => after_qed results));
 
-fun local_qed arg = local_qeds arg #> Seq.the_result finished_goal_error;
+fun local_qed arg =
+  local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
 
 
 (* global goals *)
@@ -985,26 +996,27 @@
   #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
     after_qed results (context_of state)));
 
-fun global_qed arg = global_qeds arg #> Seq.the_result finished_goal_error;
+fun global_qed arg =
+  global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
 
 
 (* concluding steps *)
 
 fun terminal_proof qeds initial terminal =
-  proof_results (SOME initial) #> Seq.maps_results (qeds terminal)
+  proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
   #> Seq.the_result "";
 
 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
-val local_default_proof = local_terminal_proof ((Method.default_text, Position.none), NONE);
-val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.none), NONE);
-fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.none), NONE);
-val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.none) (NONE, false);
+val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
+val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
+fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE);
+val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
 
 fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
-val global_default_proof = global_terminal_proof ((Method.default_text, Position.none), NONE);
-val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.none), NONE);
-fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.none), NONE);
-val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.none) (NONE, false);
+val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
+val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
+fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE);
+val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
 
 
 (* common goal statements *)