--- a/src/Pure/General/position.ML Mon Aug 23 12:25:55 2021 +0200
+++ b/src/Pure/General/position.ML Mon Aug 23 12:54:28 2021 +0200
@@ -17,7 +17,8 @@
val end_offset_of: T -> int option
val file_of: T -> string option
val id_of: T -> string option
- val advance: Symbol.symbol -> T -> T
+ val advance_symbol: Symbol.symbol -> T -> T
+ val advance_symbol_explode: string -> T -> T
val advance_offsets: int -> T -> T
val distance_of: T * T -> int option
val none: T
@@ -119,9 +120,11 @@
fun invalid_count (i, j, _: int) =
not (valid i orelse valid j);
-fun advance sym (pos as (Pos (count, props))) =
+fun advance_symbol sym (pos as (Pos (count, props))) =
if invalid_count count then pos else Pos (advance_count sym count, props);
+val advance_symbol_explode = fold advance_symbol o Symbol.explode;
+
fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
if offset = 0 orelse invalid_count count then pos
else if offset < 0 then raise Fail "Illegal offset"