# HG changeset patch
# User wenzelm
# Date 1568559695 -7200
# Node ID 437da7b72b5e628b990019f31489d523b7fd0dc2
# Parent  b080d1fb9777e37c798478c325b9b7b74fccb75b
tuned;

diff -r b080d1fb9777 -r 437da7b72b5e 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),