tuned signature (following Scala version);
authorwenzelm
Sat, 18 May 2019 13:23:36 +0200
changeset 70282 242c50877dd2
parent 70281 110df6f91376
child 70283 9ebbb53f4b50
tuned signature (following Scala version);
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;