# HG changeset patch
# User wenzelm
# Date 1680431653 -7200
# Node ID 1f990c8bb74cb10686f8bd96ec46e4303f9a5480
# Parent  5d3ce9f96cfdfd7a66f66c626c140b749202e172# Parent  99a18dcff0109d1c7abdc26ebb77b5547f2db9ee
merged

diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/Concurrent/thread_position.ML
--- a/src/Pure/Concurrent/thread_position.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/Concurrent/thread_position.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -6,7 +6,7 @@
 
 signature THREAD_POSITION =
 sig
-  type T = {line: int, offset: int, end_offset: int, props: (string * string) list}
+  type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}}
   val none: T
   val get: unit -> T
   val setmp: T -> ('a -> 'b) -> 'a -> 'b
@@ -15,11 +15,11 @@
 structure Thread_Position: THREAD_POSITION =
 struct
 
-type T = {line: int, offset: int, end_offset: int, props: (string * string) list};
+type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}};
 
 val var = Thread_Data.var () : T Thread_Data.var;
 
-val none: T = {line = 0, offset = 0, end_offset = 0, props = []};
+val none: T = {line = 0, offset = 0, end_offset = 0, props = {file = "", id = ""}};
 
 fun get () = (case Thread_Data.get var of NONE => none | SOME pos => pos);
 fun setmp pos f x = Thread_Data.setmp var (if pos = none then NONE else SOME pos) f x;
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/General/integer.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -6,6 +6,7 @@
 
 signature INTEGER =
 sig
+  val build: (int -> int) -> int
   val min: int -> int -> int
   val max: int -> int -> int
   val add: int -> int -> int
@@ -29,6 +30,8 @@
 structure Integer : INTEGER =
 struct
 
+fun build (f: int -> int) = f 0;
+
 fun min x y = Int.min (x, y);
 fun max x y = Int.max (x, y);
 
@@ -65,7 +68,7 @@
     fun shift i = swap (div_mod i base);
   in funpow_yield len shift k |> fst end;
 
-fun eval_radix base ks =
-  fold_rev (fn k => fn i => k + i * base) ks 0;
+fun eval_radix base =
+  build o fold_rev (fn k => fn i => k + i * base);
 
 end;
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/General/position.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -22,24 +22,21 @@
   val distance_of: T * T -> int option
   val none: T
   val start: T
-  val file_name: string -> Properties.T
   val file_only: string -> T
   val file: string -> T
   val line_file_only: int -> string -> T
   val line_file: int -> string -> T
   val line: int -> T
-  val get_props: T -> Properties.T
   val id: string -> T
   val id_only: string -> T
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
-  val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
-  val advance_offsets: int -> T -> T
+  val shift_offsets: {remove_id: bool} -> int -> T -> T
   val adjust_offsets: (int -> int option) -> T -> T
+  val of_props: {line: int, offset: int, end_offset: int, props: Properties.T} -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
-  val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
   val make_entity_markup: {def: bool} -> serial -> string -> string * T -> Markup.T
@@ -76,110 +73,119 @@
 
 (* datatype position *)
 
-type count = int * int * int;
-datatype T = Pos of count * Properties.T;
+datatype T = Pos of Thread_Position.T;
 
-fun dest2 f = apply2 (fn Pos p => f p);
+val make = Pos;
+fun dest (Pos args) = args;
 
 val ord =
   pointer_eq_ord
-   (int_ord o dest2 (#1 o #1) |||
-    int_ord o dest2 (#2 o #1) |||
-    int_ord o dest2 (#3 o #1) |||
-    Properties.ord o dest2 #2);
-
-fun norm_props (props: Properties.T) =
-  maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
-    [Markup.fileN, Markup.idN];
-
-fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
-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;
+   (int_ord o apply2 (#line o dest) |||
+    int_ord o apply2 (#offset o dest) |||
+    int_ord o apply2 (#end_offset o dest) |||
+    fast_string_ord o apply2 (#file o #props o dest) |||
+    fast_string_ord o apply2 (#id o #props o dest));
 
 
 (* fields *)
 
-fun line_of (Pos ((i, _, _), _)) = maybe_valid i;
-fun offset_of (Pos ((_, j, _), _)) = maybe_valid j;
-fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k;
+fun valid (i: int) = i > 0;
+fun maybe_valid i = if valid i then SOME i else NONE;
+
+val invalid = not o valid;
+fun invalid_pos (Pos {line, offset, ...}) = invalid line andalso invalid offset;
 
-fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
-fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
+val line_of = maybe_valid o #line o dest;
+val offset_of = maybe_valid o #offset o dest;
+val end_offset_of = maybe_valid o #end_offset o dest;
+
+fun file_of (Pos {props = {file, ...}, ...}) = if file = "" then NONE else SOME file;
+fun id_of (Pos {props = {id, ...}, ...}) = if id = "" then NONE else SOME id;
 
 
-(* count position *)
-
-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);
+(* symbol positions *)
 
-fun count_invalid ((i, j, _): count) = invalid i andalso invalid j;
+fun symbols [] pos = pos
+  | symbols ss (pos as Pos {line, offset, end_offset, props}) =
+      let
+        val line' = if valid line then fold (fn s => s = "\n" ? Integer.add 1) ss line else line;
+        val offset' =
+          if valid offset then fold (fn s => Symbol.not_eof s ? Integer.add 1) ss offset else offset;
+      in
+        if line = line' andalso offset = offset' then pos
+        else Pos {line = line', offset = offset', end_offset = end_offset, props = props}
+      end;
 
-fun symbol sym (pos as (Pos (count, props))) =
-  if count_invalid count then pos else Pos (count_symbol sym count, props);
+val symbol = symbols o single;
 
-val symbol_explode = fold symbol o Symbol.explode;
+fun symbol_explode str pos =
+  if str = "" orelse invalid_pos pos then pos
+  else fold symbol (Symbol.explode str) pos;
 
 
 (* distance of adjacent positions *)
 
-fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
-  if valid j andalso valid j' then SOME (j' - j) else NONE;
+fun distance_of (Pos {offset, ...}, Pos {offset = offset', ...}) =
+  if valid offset andalso valid offset' then SOME (offset' - offset) else NONE;
 
 
 (* make position *)
 
-val none = Pos ((0, 0, 0), []);
-val start = Pos ((1, 1, 0), []);
+type props = {file: string, id: string};
+
+val no_props: props = {file = "", id = ""};
+
+fun file_props name : props =
+  if name = "" then no_props else {file = name, id = ""};
+
+fun id_props id : props =
+  if id = "" then no_props else {file = "", id = id};
+
+
+val none = Pos {line = 0, offset = 0, end_offset = 0, props = no_props};
+val start = Pos {line = 1, offset = 1, end_offset = 0, props = no_props};
 
 
-fun file_name "" = []
-  | file_name name = [(Markup.fileN, name)];
+fun file_only name = Pos {line = 0, offset = 0, end_offset = 0, props = file_props name};
+fun file name = Pos {line = 1, offset = 1, end_offset = 0, props = file_props name};
 
-fun file_only name = Pos ((0, 0, 0), file_name name);
-fun file name = Pos ((1, 1, 0), file_name name);
+fun line_file_only line name = Pos {line = line, offset = 0, end_offset = 0, props = file_props name};
+fun line_file line name = Pos {line = line, offset = 1, end_offset = 0, props = file_props name};
+fun line line = line_file line "";
 
-fun line_file_only i name = Pos ((i, 0, 0), file_name name);
-fun line_file i name = Pos ((i, 1, 0), file_name name);
-fun line i = line_file i "";
+fun id id = Pos {line = 0, offset = 1, end_offset = 0, props = id_props id};
+fun id_only id = Pos {line = 0, offset = 0, end_offset = 0, props = id_props id};
 
-fun get_props (Pos (_, props)) = props;
+fun put_id id' (pos as Pos {line, offset, end_offset, props = {file, id}}) =
+  if id = id' then pos
+  else Pos {line = line, offset = offset, end_offset = end_offset, props = {file = file, id = id'}};
 
-fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
-fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
-
-fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
 fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
 fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
-fun id_properties_of pos =
-  (case id_of pos of
-    SOME id => [(Markup.idN, id)]
-  | NONE => []);
-
 
 (* adjust offsets *)
 
-fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
-  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);
+fun shift_offsets {remove_id} shift (pos as Pos {line, offset, end_offset, props}) =
+  if shift < 0 then raise Fail "Illegal offset shift"
+  else if shift > 0 andalso valid line then raise Fail "Illegal line position"
+  else
+    let
+      val offset' = if valid offset then offset + shift else offset;
+      val end_offset' = if valid end_offset then end_offset + shift else end_offset;
+      val props' = if remove_id then file_props (#file props) else props;
+    in
+      if offset = offset' andalso end_offset = end_offset' andalso props = props' then pos
+      else Pos {line = line, offset = offset', end_offset = end_offset', props = props'}
+    end;
 
-fun adjust_offsets adjust (pos as Pos (_, props)) =
+fun adjust_offsets adjust pos =
   if is_none (file_of pos) then
     (case parse_id pos of
       SOME id =>
         (case adjust id of
-          SOME offset =>
-            let val Pos (count, _) = advance_offsets offset pos
-            in Pos (count, Properties.remove Markup.idN props) end
+          SOME shift => shift_offsets {remove_id = true} shift pos
         | NONE => pos)
     | NONE => pos)
   else pos;
@@ -187,28 +193,25 @@
 
 (* markup properties *)
 
-fun get_int props name =
-  (case Properties.get props name of
-    NONE => 0
-  | SOME s => Value.parse_int s);
+fun of_props {line, offset, end_offset, props} =
+  Pos {line = line, offset = offset, end_offset = end_offset,
+    props =
+     {file = Properties.get_string props Markup.fileN,
+      id = Properties.get_string props Markup.idN}};
 
 fun of_properties props =
-  make {
-    line = get_int props Markup.lineN,
-    offset = get_int props Markup.offsetN,
-    end_offset = get_int props Markup.end_offsetN,
+  of_props {
+    line = Properties.get_int props Markup.lineN,
+    offset = Properties.get_int props Markup.offsetN,
+    end_offset = Properties.get_int props Markup.end_offsetN,
     props = props};
 
-fun int_entry k i = if invalid i then [] else [(k, Value.print_int i)];
-
-fun properties_of (Pos ((i, j, k), props)) =
-  int_entry Markup.lineN i @
-  int_entry Markup.offsetN j @
-  int_entry Markup.end_offsetN k @ props;
-
-fun offset_properties_of (Pos ((_, j, k), _)) =
-  int_entry Markup.offsetN j @
-  int_entry Markup.end_offsetN k;
+fun properties_of (Pos {line, offset, end_offset, props = {file, id}}) =
+  Properties.make_int Markup.lineN line @
+  Properties.make_int Markup.offsetN offset @
+  Properties.make_int Markup.end_offsetN end_offset @
+  Properties.make_string Markup.fileN file @
+  Properties.make_string Markup.idN id;
 
 val def_properties_of = properties_of #> map (apfst Markup.def_name);
 
@@ -279,27 +282,31 @@
 
 val no_range = (none, none);
 
-fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
-fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
+fun no_range_position (Pos {line, offset, end_offset = _, props}) =
+  Pos {line = line, offset = offset, end_offset = 0, props = props};
+
+fun range_position (Pos {line, offset, end_offset = _, props}, Pos {offset = offset', ...}) =
+  Pos {line = line, offset = offset, end_offset = offset', props = props};
+
 fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
 
 fun range_of_properties props =
   let
     val pos = of_properties props;
     val pos' =
-      make {line = get_int props Markup.end_lineN,
-        offset = get_int props Markup.end_offsetN,
+      of_props {line = Properties.get_int props Markup.end_lineN,
+        offset = Properties.get_int props Markup.end_offsetN,
         end_offset = 0,
         props = props};
   in (pos, pos') end;
 
 fun properties_of_range (pos, pos') =
-  properties_of pos @ int_entry Markup.end_lineN (the_default 0 (line_of pos'));
+  properties_of pos @ Properties.make_int Markup.end_lineN (the_default 0 (line_of pos'));
 
 
 (* thread data *)
 
-val thread_data = make o Thread_Position.get;
+val thread_data = Pos o Thread_Position.get;
 fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
 
 fun default pos =
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/General/properties.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -14,7 +14,11 @@
   val get: T -> string -> string option
   val put: entry -> T -> T
   val remove: string -> T -> T
-  val seconds: T -> string -> Time.time
+  val make_string: string -> string -> T
+  val make_int: string -> int -> T
+  val get_string: T -> string -> string
+  val get_int: T -> string -> int
+  val get_seconds: T -> string -> Time.time
 end;
 
 structure Properties: PROPERTIES =
@@ -31,8 +35,18 @@
 fun put entry (props: T) = AList.update (op =) entry props;
 fun remove name (props: T) = AList.delete (op =) name props;
 
-fun seconds props name =
-  (case AList.lookup (op =) props name of
+fun make_string k s = if s = "" then [] else [(k, s)];
+fun make_int k i = if i = 0 then [] else [(k, Value.print_int i)];
+
+val get_string = the_default "" oo get;
+
+fun get_int props name =
+  (case get props name of
+    NONE => 0
+  | SOME s => Value.parse_int s);
+
+fun get_seconds props name =
+  (case get props name of
     NONE => Time.zeroTime
   | SOME s => Time.fromReal (the_default 0.0 (Real.fromString s)));
 
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/General/set.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -82,16 +82,14 @@
 (* size *)
 
 local
-  fun add_size Empty n = n
-    | add_size (Leaf1 _) n = n + 1
-    | add_size (Leaf2 _) n = n + 2
-    | add_size (Leaf3 _) n = n + 3
-    | add_size (Branch2 (left, _, right)) n =
-        n + 1 |> add_size left |> add_size right
-    | add_size (Branch3 (left, _, mid, _, right)) n =
-        n + 2 |> add_size left |> add_size mid |> add_size right;
+  fun count Empty n = n
+    | count (Leaf1 _) n = n + 1
+    | count (Leaf2 _) n = n + 2
+    | count (Leaf3 _) n = n + 3
+    | count (Branch2 (left, _, right)) n = count right (count left (n + 1))
+    | count (Branch3 (left, _, mid, _, right)) n = count right (count mid (count left (n + 2)));
 in
-  fun size set = add_size set 0;
+  val size = Integer.build o count;
 end;
 
 
@@ -131,7 +129,7 @@
           fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))));
   in fold_rev end;
 
-fun dest tab = fold_rev_set cons tab [];
+val dest = Library.build o fold_rev_set cons;
 
 
 (* exists and forall *)
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/General/table.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -164,8 +164,8 @@
           fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))));
   in fold_rev end;
 
-fun dest tab = fold_rev_table cons tab [];
-fun keys tab = fold_rev_table (cons o #1) tab [];
+fun dest tab = Library.build (fold_rev_table cons tab);
+fun keys tab = Library.build (fold_rev_table (cons o #1) tab);
 
 
 (* min/max entries *)
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/General/value.ML
--- a/src/Pure/General/value.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/General/value.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -31,21 +31,39 @@
 
 (* nat and int *)
 
-val zero = ord "0";
-val nine = ord "9";
+local
+
+val c0 = Char.ord #"0";
+val c9 = Char.ord #"9";
+val minus = Char.ord #"-";
+
+in
+
+fun parse_int str =
+  let
+    fun err () = raise Fail ("Bad integer " ^ quote str);
+    fun char i = Char.ord (String.sub (str, i));
+    val n = size str;
 
-fun parse_nat s =
-  fold_string (fn c => fn n =>
-    let val i = ord c in
-      if zero <= i andalso i <= nine then 10 * n + (i - zero)
-      else raise Fail ("Bad natural number " ^ quote s)
-    end) s 0;
+    fun digits i a =
+      if i = n then a
+      else
+        let val c = char i
+        in if c0 <= c andalso c <= c9 then digits (i + 1) (10 * a + (c - c0)) else err () end;
+  in
+    if n = 0 then err ()
+    else if char 0 <> minus then digits 0 0
+    else if n = 1 then err ()
+    else ~ (digits 1 0)
+  end;
 
-fun parse_int s =
-  (case try (unprefix "-") s of
-    NONE => parse_nat s
-  | SOME s' => ~ (parse_nat s'))
-  handle Fail _ => raise Fail ("Bad integer " ^ quote s);
+fun parse_nat str =
+  let
+    fun err () = raise Fail ("Bad natural number " ^ quote str);
+    val i = parse_int str handle Fail _ => err ();
+  in if i >= 0 then i else err () end;
+
+end;
 
 val print_int = signed_string_of_int;
 
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/Isar/token.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -727,7 +727,7 @@
 
 fun make ((k, n), s) pos =
   let
-    val pos' = Position.advance_offsets n pos;
+    val pos' = Position.shift_offsets {remove_id = false} n pos;
     val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/ML/exn_properties.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -26,7 +26,7 @@
   | body => XML.Decode.properties body);
 
 fun position_of_polyml_location loc =
-  Position.make
+  Position.of_props
    {line = FixedInt.toInt (#startLine loc),
     offset = FixedInt.toInt (#startPosition loc),
     end_offset = FixedInt.toInt (#endPosition loc),
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -165,7 +165,9 @@
 
     (* input *)
 
-    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
+    val position_props =
+      filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.properties_of pos);
+    val location_props = op ^ (YXML.output_markup (":", position_props));
 
     val {explode_token, ...} = ML_Env.operations opt_context (#environment flags);
     fun token_content tok = if ML_Lex.is_comment tok then NONE else SOME (`explode_token tok);
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/PIDE/active.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -21,7 +21,10 @@
 
 (* active markup *)
 
-fun explicit_id () = Position.id_properties_of (Position.thread_data ());
+fun explicit_id () =
+  (case Position.id_of (Position.thread_data ()) of
+    SOME id => [(Markup.idN, id)]
+  | NONE => []);
 
 fun make_markup name {implicit, properties} =
   (name, [])
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -674,7 +674,7 @@
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
       SOME ({file = file, offset = Value.parse_int offset, name = name},
-        Properties.seconds props elapsedN)
+        Properties.get_seconds props elapsedN)
   | _ => NONE);
 
 
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -81,8 +81,8 @@
       | tree (XML.Text s) = string s;
   in tree end;
 
-fun tree_size tree = traverse (Integer.add o size) tree 0;
-fun body_size body = fold (Integer.add o tree_size) body 0;
+val tree_size = Integer.build o traverse (Integer.add o size);
+val body_size = Integer.build o fold (Integer.add o tree_size);
 
 
 (* output *)
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -38,6 +38,7 @@
 
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
+ML_file "General/integer.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
 ML_file "General/set.ML";
@@ -64,7 +65,6 @@
 
 subsection "Library of general tools";
 
-ML_file "General/integer.ML";
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/Thy/bibtex.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -25,7 +25,8 @@
   \<^scala>\<open>bibtex_check_database\<close> database
   |> YXML.parse_body
   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
-  |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
+  |> (apply2 o map o apsnd)
+      (fn pos => Position.of_properties (pos @ Position.properties_of pos0));
 
 fun check_database_output pos0 database =
   let val (errors, warnings) = check_database pos0 database in
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/Thy/latex.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -168,8 +168,8 @@
 
 in
 
-fun length_symbols syms =
-  fold Integer.add (these (read scan_latex_length syms)) 0;
+val length_symbols =
+  Integer.build o fold Integer.add o these o read scan_latex_length;
 
 fun output_symbols syms =
   if member (op =) syms Symbol.latex then
diff -r 5d3ce9f96cfd -r 1f990c8bb74c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -39,8 +39,13 @@
     segments: Document_Output.segment list};
 
 fun adjust_pos_properties (context: presentation_context) pos =
-  Position.offset_properties_of (#adjust_pos context pos) @
-  filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.get_props pos);
+  let
+    val props = Position.properties_of pos;
+    val props' = Position.properties_of (#adjust_pos context pos);
+  in
+    filter (fn (a, _) => a = Markup.offsetN orelse a = Markup.end_offsetN) props' @
+    filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) props
+  end;
 
 structure Presentation = Theory_Data
 (