# 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>\bibtex_check_database\ 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 (