tuned;
authorwenzelm
Sun, 15 Sep 2019 17:01:35 +0200
changeset 70705 437da7b72b5e
parent 70704 b080d1fb9777
child 70706 374caac3d624
tuned;
src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Sep 15 15:49:36 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 15 17:01:35 2019 +0200
@@ -177,7 +177,12 @@
 
         if (already_committed.isEmpty) (Nil, this)
         else {
-          val clean = frontier(dep_graph.maximals.filter(already_committed.keySet), Set.empty)
+          val base =
+            (for {
+              (name, (_, (_, succs))) <- dep_graph.iterator
+              if succs.isEmpty && already_committed.isDefinedAt(name)
+            } yield name).toList
+          val clean = frontier(base, Set.empty)
           if (clean.isEmpty) (Nil, this)
           else {
             (dep_graph.topological_order.filter(clean),