# HG changeset patch
# User wenzelm
# Date 1629716068 -7200
# Node ID a9e79c3645c4a484947bb8739db808e9b836ed7c
# Parent  09d4175f473e9210c8200ffc42008693091727df
clarified signature;

diff -r 09d4175f473e -r a9e79c3645c4 src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Aug 23 12:25:55 2021 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Aug 23 12:54:28 2021 +0200
@@ -82,7 +82,7 @@
 fun symbol (x : string, _ : Position.T) = x;
 
 fun explode_pos s pos = fst (fold_map (fn x => fn pos =>
-  ((x, pos), Position.advance x pos)) (raw_explode s) pos);
+  ((x, pos), Position.advance_symbol x pos)) (raw_explode s) pos);
 
 
 (** scanners **)
diff -r 09d4175f473e -r a9e79c3645c4 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Aug 23 12:25:55 2021 +0200
+++ b/src/Pure/General/position.ML	Mon Aug 23 12:54:28 2021 +0200
@@ -17,7 +17,8 @@
   val end_offset_of: T -> int option
   val file_of: T -> string option
   val id_of: T -> string option
-  val advance: Symbol.symbol -> T -> T
+  val advance_symbol: Symbol.symbol -> T -> T
+  val advance_symbol_explode: string -> T -> T
   val advance_offsets: int -> T -> T
   val distance_of: T * T -> int option
   val none: T
@@ -119,9 +120,11 @@
 fun invalid_count (i, j, _: int) =
   not (valid i orelse valid j);
 
-fun advance sym (pos as (Pos (count, props))) =
+fun advance_symbol sym (pos as (Pos (count, props))) =
   if invalid_count count then pos else Pos (advance_count sym count, props);
 
+val advance_symbol_explode = fold advance_symbol o Symbol.explode;
+
 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 09d4175f473e -r a9e79c3645c4 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon Aug 23 12:25:55 2021 +0200
+++ b/src/Pure/General/symbol_pos.ML	Mon Aug 23 12:54:28 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
+      let val pos' = List.last syms |-> Position.advance_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)) is_eof;
+  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance_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 s pos, (s, pos))))));
+    Scan.one Symbol.not_eof >> (fn s => (Position.advance_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 s1 pos1;
+        val end_pos1 = Position.advance_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 s p))
+      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance_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)))
diff -r 09d4175f473e -r a9e79c3645c4 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Aug 23 12:25:55 2021 +0200
+++ b/src/Pure/Isar/token.ML	Mon Aug 23 12:54:28 2021 +0200
@@ -381,7 +381,7 @@
 fun file_source (file: file) =
   let
     val text = cat_lines (#lines file);
-    val end_pos = fold Position.advance (Symbol.explode text) (#pos file);
+    val end_pos = Position.advance_symbol_explode text (#pos file);
   in Input.source true text (Position.range (#pos file, end_pos)) end;
 
 fun get_files (Token (_, _, Value (SOME (Files files)))) = files
diff -r 09d4175f473e -r a9e79c3645c4 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Aug 23 12:25:55 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Aug 23 12:54:28 2021 +0200
@@ -333,8 +333,8 @@
       if null syms then []
       else
         let
-          val pos1 = List.last syms |-> Position.advance;
-          val pos2 = Position.advance Symbol.space pos1;
+          val pos1 = List.last syms |-> Position.advance_symbol;
+          val pos2 = Position.advance_symbol Symbol.space pos1;
         in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
 
     fun check (Antiquote.Text tok) =
diff -r 09d4175f473e -r a9e79c3645c4 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Aug 23 12:25:55 2021 +0200
+++ b/src/Pure/Pure.thy	Mon Aug 23 12:54:28 2021 +0200
@@ -134,7 +134,7 @@
             val _ =
               (lines, pos0) |-> fold (fn line => fn pos1 =>
                 let
-                  val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
+                  val pos2 = Position.advance_symbol_explode line pos1;
                   val range = Position.range (pos1, pos2);
                   val source = Input.source true line range;
                   val _ =
@@ -144,7 +144,7 @@
                     else
                       (ignore (Resources.check_session_dir ctxt (SOME dir) source)
                         handle ERROR msg => Output.error_message msg);
-                in pos2 |> Position.advance "\n" end);
+                in pos2 |> Position.advance_symbol "\n" end);
           in thy' end)));
 
   val _ =