718 in SOME (assign_update', (command_id', exec'), init') end; |
718 in SOME (assign_update', (command_id', exec'), init') end; |
719 |
719 |
720 fun removed_execs node0 (command_id, exec_ids) = |
720 fun removed_execs node0 (command_id, exec_ids) = |
721 subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); |
721 subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); |
722 |
722 |
723 fun node_active node = |
723 fun finished_eval node = |
724 (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => |
724 let |
725 if active then NONE |
725 val active = |
726 else |
726 (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => |
727 (case opt_exec of |
727 if active then NONE |
728 NONE => SOME true |
728 else |
729 | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); |
729 (case opt_exec of |
|
730 NONE => SOME true |
|
731 | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); |
|
732 in not active end; |
730 |
733 |
731 fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context = |
734 fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context = |
732 let |
735 let |
733 val (_, offsets, rev_segments) = |
736 val (_, offsets, rev_segments) = |
734 (node, (0, Inttab.empty, [])) |-> iterate_entries |
737 (node, (0, Inttab.empty, [])) |-> iterate_entries |
767 adjust_pos = Position.adjust_offsets adjust, |
770 adjust_pos = Position.adjust_offsets adjust, |
768 segments = segments} |
771 segments = segments} |
769 end; |
772 end; |
770 |
773 |
771 fun print_consolidation options the_command_span node_name (assign_update, node) = |
774 fun print_consolidation options the_command_span node_name (assign_update, node) = |
772 (case finished_result_theory node of |
775 timeit "Document.print_consolidation" (fn () => |
773 NONE => (assign_update, node) |
776 (case finished_result_theory node of |
774 | SOME (result_id, thy) => timeit "Document.print_consolidation" (fn () => |
777 SOME (result_id, thy) => |
775 if node_active node then (assign_update, node) |
778 if finished_eval node then |
776 else |
779 let |
777 let |
780 fun commit_consolidated () = |
778 fun commit_consolidated () = |
781 (Lazy.force (get_consolidated node); |
779 (Lazy.force (get_consolidated node); |
782 Output.status [Markup.markup_only Markup.consolidated]); |
780 Output.status [Markup.markup_only Markup.consolidated]); |
783 val consolidation = |
781 val consolidation = |
784 if Options.bool options \<^system_option>\<open>pide_presentation\<close> then |
782 if Options.bool options \<^system_option>\<open>pide_presentation\<close> then |
785 let val context = presentation_context options the_command_span node_name node in |
783 let val context = presentation_context options the_command_span node_name node in |
786 fn _ => |
784 fn _ => |
787 let |
|
788 val _ = Output.status [Markup.markup_only Markup.consolidating]; |
|
789 val res = Exn.capture (Thy_Info.apply_presentation context) thy; |
|
790 val _ = commit_consolidated (); |
|
791 in Exn.release res end |
|
792 end |
|
793 else fn _ => commit_consolidated (); |
|
794 |
|
795 val result_entry = |
|
796 (case lookup_entry node result_id of |
|
797 NONE => err_undef "result command entry" result_id |
|
798 | SOME (eval, prints) => |
785 let |
799 let |
786 val _ = Output.status [Markup.markup_only Markup.consolidating]; |
800 val print = eval |> Command.print0 |
787 val res = Exn.capture (Thy_Info.apply_presentation context) thy; |
801 {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation}; |
788 val _ = commit_consolidated (); |
802 in (result_id, SOME (eval, print :: prints)) end); |
789 in Exn.release res end |
803 |
790 end |
804 val assign_update' = assign_update |> assign_update_change result_entry; |
791 else fn _ => commit_consolidated (); |
805 val node' = node |> assign_entry result_entry; |
792 |
806 in (assign_update', node') end |
793 val result_entry = |
807 else (assign_update, node) |
794 (case lookup_entry node result_id of |
808 | NONE => (assign_update, node))); |
795 NONE => err_undef "result command entry" result_id |
809 |
796 | SOME (eval, prints) => |
|
797 let |
|
798 val print = eval |> Command.print0 |
|
799 {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation}; |
|
800 in (result_id, SOME (eval, print :: prints)) end); |
|
801 |
|
802 val assign_update' = assign_update |> assign_update_change result_entry; |
|
803 val node' = node |> assign_entry result_entry; |
|
804 in (assign_update', node') end)); |
|
805 in |
810 in |
806 |
811 |
807 fun update old_version_id new_version_id edits consolidate state = |
812 fun update old_version_id new_version_id edits consolidate state = |
808 Runtime.exn_trace_system (fn () => |
813 Runtime.exn_trace_system (fn () => |
809 let |
814 let |