# HG changeset patch
# User wenzelm
# Date 1680353443 -7200
# Node ID 279b18bb4059cdae77576de5720807fbb4154ae1
# Parent  472e48ed9c7985d74a9f742fdce0f93b98c33a81
clarified signature;

diff -r 472e48ed9c79 -r 279b18bb4059 src/Pure/General/position.ML
--- 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
diff -r 472e48ed9c79 -r 279b18bb4059 src/Pure/Isar/token.ML
--- 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