--- a/src/Pure/General/position.ML Sat Apr 01 14:32:02 2023 +0200
+++ b/src/Pure/General/position.ML Sat Apr 01 14:50:43 2023 +0200
@@ -35,7 +35,7 @@
val copy_id: T -> T -> T
val id_properties_of: T -> Properties.T
val parse_id: T -> int option
- val advance_offsets: int -> T -> T
+ val shift_offsets: {remove_id: bool} -> int -> T -> T
val adjust_offsets: (int -> int option) -> T -> T
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
@@ -188,8 +188,6 @@
else Pos {line = line, offset = offset', end_offset = end_offset', props = props'}
end;
-val advance_offsets = shift_offsets {remove_id = false};
-
fun adjust_offsets adjust pos =
if is_none (file_of pos) then
(case parse_id pos of
--- a/src/Pure/Isar/token.ML Sat Apr 01 14:32:02 2023 +0200
+++ b/src/Pure/Isar/token.ML Sat Apr 01 14:50:43 2023 +0200
@@ -727,7 +727,7 @@
fun make ((k, n), s) pos =
let
- val pos' = Position.advance_offsets n pos;
+ val pos' = Position.shift_offsets {remove_id = false} n pos;
val range = Position.range (pos, pos');
val tok =
if 0 <= k andalso k < Vector.length immediate_kinds then