# 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