--- a/src/Pure/General/position.ML Wed Dec 03 15:22:27 2014 +0100
+++ b/src/Pure/General/position.ML Wed Dec 03 20:45:20 2014 +0100
@@ -14,6 +14,7 @@
val end_offset_of: T -> int option
val file_of: T -> string option
val advance: Symbol.symbol -> T -> T
+ val advance_offset: int -> T -> T
val distance_of: T -> T -> int
val none: T
val start: T
@@ -101,6 +102,11 @@
fun advance sym (pos as (Pos (count, props))) =
if invalid_count count then pos else Pos (advance_count sym count, props);
+fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
+ if invalid_count count then pos
+ else if valid i then raise Fail "Illegal line position"
+ else Pos ((i, if_valid j (j + offset), k), props);
+
(* distance of adjacent positions *)