--- 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 **)
--- 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
--- 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)))
--- 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
--- 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) =
--- 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 _ =
--- 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 -}