--- a/src/Pure/PIDE/document.ML Fri Nov 04 16:51:07 2022 +0100
+++ b/src/Pure/PIDE/document.ML Fri Nov 04 16:59:56 2022 +0100
@@ -724,7 +724,7 @@
let
val (_, offsets, rev_segments) =
(node, (0, Inttab.empty, [])) |-> iterate_entries
- (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) =>
+ (fn ((prev, id), opt_exec) => fn (offset, offsets, segments) =>
(case opt_exec of
SOME (eval, _) =>
let
@@ -746,7 +746,7 @@
|> Inttab.update (exec_id, offset);
val segments' = (span, (st, tr, st')) :: segments;
in SOME (offset', offsets', segments') end
- | NONE => NONE));
+ | NONE => raise Fail ("Unassigned exec " ^ Value.print_int id)));
val adjust = Inttab.lookup offsets;
val segments =