# HG changeset patch
# User wenzelm
# Date 1439305583 -7200
# Node ID bd743ec4033413bf323e740b515eaaa036a178c6
# Parent  3c8b9b4b577cb30795fb65ace3560616916430f1
clarified break *point* position;

diff -r 3c8b9b4b577c -r bd743ec40334 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Tue Aug 11 17:00:16 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Tue Aug 11 17:06:23 2015 +0200
@@ -90,7 +90,7 @@
       | breakpoints loc pt =
           (case ML_Parse_Tree.breakpoint pt of
             SOME b =>
-              let val pos = Exn_Properties.position_of loc in
+              let val pos = Position.reset_range (Exn_Properties.position_of loc) in
                 if is_reported pos then
                   let val id = serial ();
                   in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end