proper range position;
authorwenzelm
Wed Jan 16 18:43:59 2013 +0100 (2013-01-16)
changeset 509128d391f185cac
parent 50911 ee7fe4230642
child 50913 697e3bb60a3b
proper range position;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Jan 16 16:26:36 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jan 16 18:43:59 2013 +0100
     1.3 @@ -827,7 +827,8 @@
     1.4      val (finish_text, terminal_pos, finished_pos) =
     1.5        (case opt_text of
     1.6          NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
     1.7 -      | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
     1.8 +      | SOME (text, (pos, end_pos)) =>
     1.9 +          (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
    1.10    in
    1.11      Seq.APPEND (fn state =>
    1.12        state