prefer strict operation;
authorwenzelm
Fri, 04 Nov 2022 16:59:56 +0100
changeset 76434 f29056da5903
parent 76433 b1ab7bf41d88
child 76435 0901321dd6b2
prefer strict operation;
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 =