# HG changeset patch
# User wenzelm
# Date 1358358239 -3600
# Node ID 8d391f185caccfc606dee811f2bd8a95e5ca0796
# Parent  ee7fe4230642f1023ae641bcacd2de6b66577cb1
proper range position;

diff -r ee7fe4230642 -r 8d391f185cac src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jan 16 16:26:36 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Jan 16 18:43:59 2013 +0100
@@ -827,7 +827,8 @@
     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));
+      | SOME (text, (pos, end_pos)) =>
+          (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
   in
     Seq.APPEND (fn state =>
       state