# HG changeset patch
# User wenzelm
# Date 1558178616 -7200
# Node ID 242c50877dd2498113e9260865bbcb9ec2b151e9
# Parent  110df6f913766353ab90a96cc55150e23770179e
tuned signature (following Scala version);

diff -r 110df6f91376 -r 242c50877dd2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat May 18 12:08:30 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Sat May 18 13:23:36 2019 +0200
@@ -294,11 +294,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) =
+  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 String_Graph.is_maximal nodes1 name andalso is_empty_node node
+      if is_suppressed_node nodes1 (name, node)
       then String_Graph.del_node name nodes1
       else nodes1;
   in Version nodes2 end;