changeset 72707 | f1380c9f3806 |
parent 72706 | 52d0b5fcb19d |
child 73864 | ac5a72740f3a |
--- a/src/Pure/General/position.ML Wed Nov 25 13:51:28 2020 +0100 +++ b/src/Pure/General/position.ML Wed Nov 25 15:12:02 2020 +0100 @@ -90,7 +90,7 @@ fun norm_props (props: Properties.T) = maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) - Markup.position_properties'; + [Markup.fileN, Markup.idN]; fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props); fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};