src/Pure/PIDE/headless.scala
changeset 70705 437da7b72b5e
parent 70704 b080d1fb9777
child 70710 3f557ed88fd6
equal deleted inserted replaced
70704:b080d1fb9777 70705:437da7b72b5e
   175           }
   175           }
   176         }
   176         }
   177 
   177 
   178         if (already_committed.isEmpty) (Nil, this)
   178         if (already_committed.isEmpty) (Nil, this)
   179         else {
   179         else {
   180           val clean = frontier(dep_graph.maximals.filter(already_committed.keySet), Set.empty)
   180           val base =
       
   181             (for {
       
   182               (name, (_, (_, succs))) <- dep_graph.iterator
       
   183               if succs.isEmpty && already_committed.isDefinedAt(name)
       
   184             } yield name).toList
       
   185           val clean = frontier(base, Set.empty)
   181           if (clean.isEmpty) (Nil, this)
   186           if (clean.isEmpty) (Nil, this)
   182           else {
   187           else {
   183             (dep_graph.topological_order.filter(clean),
   188             (dep_graph.topological_order.filter(clean),
   184               copy(dep_graph = dep_graph.exclude(clean)))
   189               copy(dep_graph = dep_graph.exclude(clean)))
   185           }
   190           }