# HG changeset patch
# User wenzelm
# Date 1570437899 -7200
# Node ID da647a0c8313e402dffe6ac8378e3ea5b0509ea0
# Parent  ea2834adf8de501470155dc393ac28de40dcef3e
clarified signature;

diff -r ea2834adf8de -r da647a0c8313 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sun Oct 06 19:33:58 2019 +0200
+++ b/src/Pure/General/graph.scala	Mon Oct 07 10:44:59 2019 +0200
@@ -112,20 +112,25 @@
   /* reachability */
 
   /*reachable nodes with length of longest path*/
-  def reachable_length(next: Key => Keys, xs: List[Key]): Map[Key, Int] =
+  def reachable_length(
+    count: Key => Int,
+    next: Key => Keys,
+    xs: List[Key]): Map[Key, Int] =
   {
     def reach(length: Int)(rs: Map[Key, Int], x: Key): Map[Key, Int] =
       if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs
-      else ((rs + (x -> length)) /: next(x))(reach(length + 1))
+      else ((rs + (x -> length)) /: next(x))(reach(length + count(x)))
     (Map.empty[Key, Int] /: xs)(reach(0))
   }
-  def node_height: Map[Key, Int] = reachable_length(imm_preds(_), maximals)
-  def node_depth: Map[Key, Int] = reachable_length(imm_succs(_), minimals)
+  def node_height(count: Key => Int): Map[Key, Int] =
+    reachable_length(count, imm_preds(_), maximals)
+  def node_depth(count: Key => Int): Map[Key, Int] =
+    reachable_length(count, imm_succs(_), minimals)
 
   /*reachable nodes with size limit*/
   def reachable_limit(
     limit: Int,
-    count: Key => Boolean,
+    count: Key => Int,
     next: Key => Keys,
     xs: List[Key]): Keys =
   {
@@ -133,7 +138,7 @@
     {
       val (n, rs) = res
       if (rs.contains(x)) res
-      else ((if (count(x)) n + 1 else n, rs + x) /: next(x))(reach _)
+      else ((n + count(x), rs + x) /: next(x))(reach _)
     }
 
     @tailrec def reachs(size: Int, rs: Keys, rest: List[Key]): Keys =
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