diff -r ea2834adf8de -r da647a0c8313 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Oct 06 19:33:58 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Oct 07 10:44:59 2019 +0200
@@ -59,7 +59,7 @@
         val pending = maximals.filterNot(finished)
         if (pending.isEmpty || pending.tail.isEmpty) pending
         else {
-          val depth = dep_graph.node_depth
+          val depth = dep_graph.node_depth(_ => 1)
           pending.sortBy(node => - depth(node))
         }
       }
@@ -78,7 +78,7 @@
           ((requirements, share_common_data), Load_Bulk(pending, Nil, checkpoints))
         }
         else {
-          def count(node: Document.Node.Name): Boolean = !finished(node)
+          def count(node: Document.Node.Name): Int = if (finished(node)) 0 else 1
           val reachable = dep_graph.reachable_limit(limit, count _, dep_graph.imm_preds, pending)
           val (pending1, pending2) = pending.partition(reachable)
           val requirements = dep_graph.all_preds(pending1).reverse