# HG changeset patch
# User wenzelm
# Date 1629721497 -7200
# Node ID a3b0fc51070562cec2f01374df63910396fe606b
# Parent  8d03d548df1c9c926a1b45e2b673fdc971ffe3fd
clarified signature;

diff -r 8d03d548df1c -r a3b0fc510705 src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Aug 23 14:24:57 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_symbol x pos)) (raw_explode s) pos);
+  ((x, pos), Position.symbol x pos)) (raw_explode s) pos);
 
 
 (** scanners **)
diff -r 8d03d548df1c -r a3b0fc510705 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/Pure/General/position.ML	Mon Aug 23 14:24:57 2021 +0200
@@ -17,8 +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.symbol -> T -> T
-  val advance_symbol_explode: string -> T -> T
+  val symbol: Symbol.symbol -> T -> T
+  val symbol_explode: string -> T -> T
   val advance_offsets: int -> T -> T
   val distance_of: T * T -> int option
   val none: T
@@ -120,10 +120,10 @@
 fun invalid_count (i, j, _: int) =
   not (valid i orelse valid j);
 
-fun advance_symbol sym (pos as (Pos (count, props))) =
+fun 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;
+val symbol_explode = fold 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
diff -r 8d03d548df1c -r a3b0fc510705 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)))
diff -r 8d03d548df1c -r a3b0fc510705 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/Pure/Isar/token.ML	Mon Aug 23 14:24:57 2021 +0200
@@ -381,7 +381,7 @@
 fun file_source (file: file) =
   let
     val text = cat_lines (#lines file);
-    val end_pos = Position.advance_symbol_explode text (#pos file);
+    val end_pos = Position.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 8d03d548df1c -r a3b0fc510705 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Aug 23 14:24:57 2021 +0200
@@ -333,8 +333,8 @@
       if null syms then []
       else
         let
-          val pos1 = List.last syms |-> Position.advance_symbol;
-          val pos2 = Position.advance_symbol Symbol.space pos1;
+          val pos1 = List.last syms |-> Position.symbol;
+          val pos2 = Position.symbol Symbol.space pos1;
         in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
 
     fun check (Antiquote.Text tok) =
diff -r 8d03d548df1c -r a3b0fc510705 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/Pure/Pure.thy	Mon Aug 23 14:24:57 2021 +0200
@@ -134,7 +134,7 @@
             val _ =
               (lines, pos0) |-> fold (fn line => fn pos1 =>
                 let
-                  val pos2 = Position.advance_symbol_explode line pos1;
+                  val pos2 = Position.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_symbol "\n" end);
+                in pos2 |> Position.symbol "\n" end);
           in thy' end)));
 
   val _ =
diff -r 8d03d548df1c -r a3b0fc510705 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Aug 23 13:23:48 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Mon Aug 23 14:24:57 2021 +0200
@@ -1170,7 +1170,7 @@
 module Isabelle.Position (
   T, line_of, column_of, offset_of, end_offset_of, file_of, id_of,
   start, none, put_file, file, file_only, put_id,
-  advance_symbol, advance_symbol_explode, advance_symbol_explode_string, shift_offsets,
+  symbol, symbol_explode, symbol_explode_string, shift_offsets,
   of_properties, properties_of, def_properties_of, entity_markup, entity_properties_of,
   is_reported, is_reported_range, here,
 
@@ -1261,18 +1261,18 @@
 advance_offset :: Symbol -> Int -> Int
 advance_offset c offset = if_valid offset (offset + 1)
 
-advance_symbol :: Symbol -> T -> T
-advance_symbol s pos =
+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) }
 
-advance_symbol_explode :: BYTES a => a -> T -> T
-advance_symbol_explode = fold advance_symbol . Symbol.explode . make_bytes
-
-advance_symbol_explode_string :: String -> T -> T
-advance_symbol_explode_string = advance_symbol_explode
+symbol_explode :: BYTES a => a -> T -> T
+symbol_explode = fold symbol . Symbol.explode . make_bytes
+
+symbol_explode_string :: String -> T -> T
+symbol_explode_string = symbol_explode
 
 
 {- shift offsets -}