# HG changeset patch
# User wenzelm
# Date 1629744022 -7200
# Node ID b707145300458b9f36c44271961f594540afc9e4
# Parent  53e28c438f967ad967dfd5f032dd6b63fcd20bd9
tuned;

diff -r 53e28c438f96 -r b70714530045 src/Pure/General/position.ML
--- 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"
diff -r 53e28c438f96 -r b70714530045 src/Tools/Haskell/Haskell.thy
--- 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