# HG changeset patch
# User wenzelm
# Date 1629801109 -7200
# Node ID 5d40a4f66fddc40dcdb59cb9b2449e1c2838de27
# Parent  54e096758b6385595bfa787c1a2ea142e730abdf
tuned;

diff -r 54e096758b63 -r 5d40a4f66fdd src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 24 12:28:07 2021 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 24 12:31:49 2021 +0200
@@ -19,7 +19,6 @@
   val id_of: T -> string option
   val symbol: Symbol.symbol -> T -> T
   val symbol_explode: string -> T -> T
-  val advance_offsets: int -> T -> T
   val distance_of: T * T -> int option
   val none: T
   val start: T
@@ -36,6 +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 adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
@@ -126,15 +126,6 @@
 val symbol_explode = fold symbol o Symbol.explode;
 
 
-(* advance offsets *)
-
-fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
-  if offset = 0 orelse count_invalid count then pos
-  else if offset < 0 then raise Fail "Illegal offset"
-  else if valid i then raise Fail "Illegal line position"
-  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
-
-
 (* distance of adjacent positions *)
 
 fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
@@ -172,6 +163,15 @@
     SOME id => [(Markup.idN, id)]
   | NONE => []);
 
+
+(* adjust offsets *)
+
+fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
+  if offset = 0 orelse count_invalid count then pos
+  else if offset < 0 then raise Fail "Illegal offset"
+  else if valid i then raise Fail "Illegal line position"
+  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
+
 fun adjust_offsets adjust (pos as Pos (_, props)) =
   if is_none (file_of pos) then
     (case parse_id pos of