src/Pure/General/symbol_pos.ML

--- a/src/Pure/General/symbol_pos.ML	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/Pure/General/symbol_pos.ML	Mon Aug 23 14:24:57 2021 +0200
@@ -62,7 +62,7 @@
 val content = implode o map symbol;
 
 fun range (syms as (_, pos) :: _) =
-      let val pos' = List.last syms |-> Position.advance_symbol
+      let val pos' = List.last syms |-> Position.symbol
       in Position.range (pos, pos') end
   | range [] = Position.no_range;
 
@@ -75,7 +75,7 @@
 val is_eof = Symbol.is_eof o symbol;
 
 val stopper =
-  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance_symbol)) is_eof;
+  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.symbol)) is_eof;
 
 
 (* basic scanners *)
@@ -233,7 +233,7 @@
 
 fun source pos =
   Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos =>
-    Scan.one Symbol.not_eof >> (fn s => (Position.advance_symbol s pos, (s, pos))))));
+    Scan.one Symbol.not_eof >> (fn s => (Position.symbol s pos, (s, pos))))));
 
 
 (* compact representation -- with Symbol.DEL padding *)
@@ -244,7 +244,7 @@
   | pad [(s, _)] = [s]
   | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
       let
-        val end_pos1 = Position.advance_symbol s1 pos1;
+        val end_pos1 = Position.symbol s1 pos1;
         val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
       in s1 :: replicate d Symbol.DEL @ pad rest end;
 
@@ -257,7 +257,7 @@
 fun explode_delete (str, pos) =
   let
     val (res, _) =
-      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance_symbol s p))
+      fold (fn s => fn (res, p) => ((s, p) :: res, Position.symbol s p))
         (Symbol.explode str) ([], Position.no_range_position pos);
   in
     fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p)))