# HG changeset patch
# User wenzelm
# Date 1568365259 -7200
# Node ID 5d32cca55c2a2b52060f109b554f41f4a21a90e1
# Parent  0fec12eabad0f2459e087d3c6a545626a00455f8
tuned;

diff -r 0fec12eabad0 -r 5d32cca55c2a src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Sep 12 17:17:52 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Sep 13 11:00:59 2019 +0200
@@ -193,15 +193,13 @@
   map_node (fn (header, keywords, perspective, entries, result, _) =>
     (header, keywords, perspective, entries, result, Lazy.lazy I));
 
-fun get_consolidated (Node {consolidated, ...}) = consolidated;
+fun commit_consolidated (Node {consolidated, ...}) =
+  (Lazy.force consolidated; Output.status [Markup.markup_only Markup.consolidated]);
 
-val is_consolidated = Lazy.is_finished o get_consolidated;
-
-fun commit_consolidated node =
-  (Lazy.force (get_consolidated node); Output.status [Markup.markup_only Markup.consolidated]);
+fun consolidated_node (Node {consolidated, ...}) = Lazy.is_finished consolidated;
 
 fun could_consolidate node =
-  not (is_consolidated node) andalso is_some (finished_result_theory node);
+  not (consolidated_node 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;
@@ -299,14 +297,14 @@
       (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits))
       nodes);
 
-fun is_suppressed_node (nodes: node String_Graph.T) (name, node) =
+fun suppressed_node (nodes: node String_Graph.T) (name, node) =
   String_Graph.is_maximal nodes name andalso is_empty_node node;
 
 fun put_node (name, node) (Version nodes) =
   let
     val nodes1 = update_node name (K node) nodes;
     val nodes2 =
-      if is_suppressed_node nodes1 (name, node)
+      if suppressed_node nodes1 (name, node)
       then String_Graph.del_node name nodes1
       else nodes1;
   in Version nodes2 end;