# HG changeset patch
# User wenzelm
# Date 1667577596 -3600
# Node ID f29056da5903526101fb90e277a6b12150841650
# Parent  b1ab7bf41d88f864594c13cf7a04658d61f76908
prefer strict operation;

diff -r b1ab7bf41d88 -r f29056da5903 src/Pure/PIDE/document.ML
--- 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 =