--- 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;
--- 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;
--- 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 =
--- 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)));
--- 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 *)
--- 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 *)
--- 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;
--- 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
--- 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),
--- 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);
--- 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, [])
--- 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);
--- 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 *)
--- 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";
--- 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
--- 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
--- 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
(