# HG changeset patch
# User wenzelm
# Date 1667577067 -3600
# Node ID b1ab7bf41d88f864594c13cf7a04658d61f76908
# Parent  d0079b509d996e2fabd46dff9a0c5b7080c6ac32
tuned;

diff -r d0079b509d99 -r b1ab7bf41d88 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 04 16:35:39 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 04 16:51:07 2022 +0100
@@ -723,29 +723,30 @@
 fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context =
   let
     val (_, offsets, rev_segments) =
-      iterate_entries (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) =>
-        (case opt_exec of
-          SOME (eval, _) =>
-            let
-              val command_id = Command.eval_command_id eval;
-              val span = the_command_span command_id;
-
-              val st =
-                (case try (#1 o the o the_entry node o the) prev of
-                  NONE => Toplevel.make_state NONE
-                | SOME prev_eval => Command.eval_result_state prev_eval);
+      (node, (0, Inttab.empty, [])) |-> iterate_entries
+        (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) =>
+          (case opt_exec of
+            SOME (eval, _) =>
+              let
+                val command_id = Command.eval_command_id eval;
+                val span = the_command_span command_id;
 
-              val exec_id = Command.eval_exec_id eval;
-              val tr = Command.eval_result_command eval;
-              val st' = Command.eval_result_state eval;
+                val st =
+                  (case try (#1 o the o the_entry node o the) prev of
+                    NONE => Toplevel.make_state NONE
+                  | SOME prev_eval => Command.eval_result_state prev_eval);
 
-              val offset' = offset + the_default 0 (Command_Span.symbol_length span);
-              val offsets' = offsets
-                |> Inttab.update (command_id, offset)
-                |> Inttab.update (exec_id, offset);
-              val segments' = (span, (st, tr, st')) :: segments;
-            in SOME (offset', offsets', segments') end
-        | NONE => NONE)) node (0, Inttab.empty, []);
+                val exec_id = Command.eval_exec_id eval;
+                val tr = Command.eval_result_command eval;
+                val st' = Command.eval_result_state eval;
+
+                val offset' = offset + the_default 0 (Command_Span.symbol_length span);
+                val offsets' = offsets
+                  |> Inttab.update (command_id, offset)
+                  |> Inttab.update (exec_id, offset);
+                val segments' = (span, (st, tr, st')) :: segments;
+              in SOME (offset', offsets', segments') end
+          | NONE => NONE));
 
     val adjust = Inttab.lookup offsets;
     val segments =