# HG changeset patch # User wenzelm # Date 1667487824 -3600 # Node ID e4f164d864dc9fb5b87df1a9f8bc296409d83321 # Parent 3f16fc68f0f0660dda03c46e6c6ba7f4d7b31e9d more timing; diff -r 3f16fc68f0f0 -r e4f164d864dc src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Nov 03 15:19:01 2022 +0100 +++ b/src/Pure/PIDE/document.ML Thu Nov 03 16:03:44 2022 +0100 @@ -731,84 +731,85 @@ fun print_consolidation options the_command_span node_name (assign_update, node) = (case finished_result_theory node of SOME (result_id, thy) => - let - val active_tasks = - (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => - if active then NONE - else - (case opt_exec of - NONE => NONE - | SOME (eval, _) => - SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); - in - if not active_tasks then - let - fun commit_consolidated () = - (Lazy.force (get_consolidated node); - Output.status [Markup.markup_only Markup.consolidated]); - val consolidation = - if Options.bool options "editor_presentation" then - 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; + timeit "Document.print_consolidation" (fn () => + let + val active_tasks = + (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => + if active then NONE + else + (case opt_exec of + NONE => NONE + | SOME (eval, _) => + SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); + in + if not active_tasks then + let + fun commit_consolidated () = + (Lazy.force (get_consolidated node); + Output.status [Markup.markup_only Markup.consolidated]); + val consolidation = + if Options.bool options "editor_presentation" then + 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.init_toplevel () - | SOME prev_eval => Command.eval_result_state prev_eval); + val st = + (case try (#1 o the o the_entry node o the) prev of + NONE => Toplevel.init_toplevel () + | SOME prev_eval => Command.eval_result_state prev_eval); - val exec_id = Command.eval_exec_id eval; - val tr = Command.eval_result_command eval; - val st' = Command.eval_result_state eval; + 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)) node (0, Inttab.empty, []); + 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 adjust = Inttab.lookup offsets; + val segments = + rev rev_segments |> map (fn (span, (st, tr, st')) => + {span = Command_Span.adjust_offsets adjust span, + prev_state = st, command = tr, state = st'}); - val adjust = Inttab.lookup offsets; - val segments = - rev rev_segments |> map (fn (span, (st, tr, st')) => - {span = Command_Span.adjust_offsets adjust span, - prev_state = st, command = tr, state = st'}); + val presentation_context: Thy_Info.presentation_context = + {options = options, + file_pos = Position.file node_name, + adjust_pos = Position.adjust_offsets adjust, + segments = segments}; + in + fn _ => + let + val _ = Output.status [Markup.markup_only Markup.consolidating]; + val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy; + val _ = commit_consolidated (); + in Exn.release res end + end + else fn _ => commit_consolidated (); - val presentation_context: Thy_Info.presentation_context = - {options = options, - file_pos = Position.file node_name, - adjust_pos = Position.adjust_offsets adjust, - segments = segments}; - in - fn _ => + val result_entry = + (case lookup_entry node result_id of + NONE => err_undef "result command entry" result_id + | SOME (eval, prints) => let - val _ = Output.status [Markup.markup_only Markup.consolidating]; - val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy; - val _ = commit_consolidated (); - in Exn.release res end - end - else fn _ => commit_consolidated (); + val print = eval |> Command.print0 + {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation}; + in (result_id, SOME (eval, print :: prints)) end); - val result_entry = - (case lookup_entry node result_id of - NONE => err_undef "result command entry" result_id - | SOME (eval, prints) => - let - val print = eval |> Command.print0 - {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation}; - in (result_id, SOME (eval, print :: prints)) end); - - val assign_update' = assign_update |> assign_update_change result_entry; - val node' = node |> assign_entry result_entry; - in (assign_update', node') end - else (assign_update, node) - end + val assign_update' = assign_update |> assign_update_change result_entry; + val node' = node |> assign_entry result_entry; + in (assign_update', node') end + else (assign_update, node) + end) | NONE => (assign_update, node)); in