--- a/src/Pure/General/position.ML Mon Aug 23 20:18:00 2021 +0200
+++ b/src/Pure/General/position.ML Mon Aug 23 20:40:22 2021 +0200
@@ -109,22 +109,24 @@
fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
-(* advance *)
+(* count position *)
-fun advance_count "\n" (i: int, j: int, k: int) =
+fun count_symbol "\n" (i: int, j: int, k: int) =
(if_valid i (i + 1), if_valid j (j + 1), k)
- | advance_count s (i, j, k) =
- if Symbol.not_eof s then (i, if_valid j (j + 1), k)
- else (i, j, k);
+ | count_symbol s (i, j, k) =
+ if Symbol.not_eof s then (i, if_valid j (j + 1), k) else (i, j, k);
fun invalid_count (i, j, _: int) =
not (valid i orelse valid j);
fun symbol sym (pos as (Pos (count, props))) =
- if invalid_count count then pos else Pos (advance_count sym count, props);
+ if invalid_count count then pos else Pos (count_symbol sym count, props);
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 invalid_count count then pos
else if offset < 0 then raise Fail "Illegal offset"
--- a/src/Tools/Haskell/Haskell.thy Mon Aug 23 20:18:00 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Mon Aug 23 20:40:22 2021 +0200
@@ -1248,25 +1248,25 @@
put_id id pos = pos { _id = id }
-{- advance position -}
-
-advance_line :: Symbol -> Int -> Int
-advance_line "\n" line = if_valid line (line + 1)
-advance_line _ line = line
-
-advance_column :: Symbol -> Int -> Int
-advance_column "\n" column = if_valid column 1
-advance_column _ column = if_valid column (column + 1)
-
-advance_offset :: Symbol -> Int -> Int
-advance_offset c offset = if_valid offset (offset + 1)
+{- count position -}
+
+count_line :: Symbol -> Int -> Int
+count_line "\n" line = if_valid line (line + 1)
+count_line _ line = line
+
+count_column :: Symbol -> Int -> Int
+count_column "\n" column = if_valid column 1
+count_column _ column = if_valid column (column + 1)
+
+count_offset :: Symbol -> Int -> Int
+count_offset _ offset = if_valid offset (offset + 1)
symbol :: Symbol -> T -> T
symbol s pos =
pos {
- _line = advance_line s (_line pos),
- _column = advance_column s (_column pos),
- _offset = advance_offset s (_offset pos) }
+ _line = count_line s (_line pos),
+ _column = count_column s (_column pos),
+ _offset = count_offset s (_offset pos) }
symbol_explode :: BYTES a => a -> T -> T
symbol_explode = fold symbol . Symbol.explode . make_bytes