clarified break *point* position;
authorwenzelm
Tue, 11 Aug 2015 17:06:23 +0200
changeset 60894 bd743ec40334
parent 60893 3c8b9b4b577c
child 60895 501be4aa75b4
clarified break *point* position;
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