# HG changeset patch # User wenzelm # Date 1667485141 -3600 # Node ID 3f16fc68f0f0660dda03c46e6c6ba7f4d7b31e9d # Parent cc3911b11b53db6f74c54a57b3f994ca002d48ff tuned; diff -r cc3911b11b53 -r 3f16fc68f0f0 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Nov 03 14:50:43 2022 +0100 +++ b/src/Pure/PIDE/document.ML Thu Nov 03 15:19:01 2022 +0100 @@ -188,17 +188,15 @@ in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end else NONE; +fun get_consolidated (Node {consolidated, ...}) = consolidated; + val reset_consolidated = map_node (fn (header, keywords, perspective, entries, result, _) => (header, keywords, perspective, entries, result, Lazy.lazy I)); -fun commit_consolidated (Node {consolidated, ...}) = - (Lazy.force consolidated; Output.status [Markup.markup_only Markup.consolidated]); - -fun consolidated_node (Node {consolidated, ...}) = Lazy.is_finished consolidated; - fun could_consolidate node = - not (consolidated_node node) andalso is_some (finished_result_theory node); + not (Lazy.is_finished (get_consolidated node)) andalso + is_some (finished_result_theory node); fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; @@ -745,6 +743,9 @@ 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 @@ -789,10 +790,10 @@ let val _ = Output.status [Markup.markup_only Markup.consolidating]; val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy; - val _ = commit_consolidated node; + val _ = commit_consolidated (); in Exn.release res end end - else fn _ => commit_consolidated node; + else fn _ => commit_consolidated (); val result_entry = (case lookup_entry node result_id of