# HG changeset patch
# User wenzelm
# Date 1629800887 -7200
# Node ID 54e096758b6385595bfa787c1a2ea142e730abdf
# Parent  5f81ebfb551e0cf0607098e8c3e3518b60815941
tuned signature;

diff -r 5f81ebfb551e -r 54e096758b63 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 24 12:11:57 2021 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 24 12:28:07 2021 +0200
@@ -76,7 +76,8 @@
 
 (* datatype position *)
 
-datatype T = Pos of (int * int * int) * Properties.T;
+type count = int * int * int;
+datatype T = Pos of count * Properties.T;
 
 fun dest2 f = apply2 (fn Pos p => f p);
 
@@ -95,6 +96,7 @@
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
 
 fun valid (i: int) = i > 0;
+val invalid = not o valid;
 fun maybe_valid i = if valid i then SOME i else NONE;
 fun if_valid i i' = if valid i then i' else i;
 
@@ -111,16 +113,15 @@
 
 (* count position *)
 
-fun count_symbol "\n" (i: int, j: int, k: int) =
+fun count_symbol "\n" ((i, j, k): count) =
       (if_valid i (i + 1), if_valid j (j + 1), 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 count_invalid ((i, j, _): count) = invalid i andalso invalid j;
 
 fun symbol sym (pos as (Pos (count, props))) =
-  if invalid_count count then pos else Pos (count_symbol sym count, props);
+  if count_invalid count then pos else Pos (count_symbol sym count, props);
 
 val symbol_explode = fold symbol o Symbol.explode;
 
@@ -128,7 +129,7 @@
 (* advance offsets *)
 
 fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
-  if offset = 0 orelse invalid_count count then pos
+  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);