src/Pure/PIDE/headless.scala
changeset 70795 a90e40118874
parent 70794 da647a0c8313
child 70796 2739631ac368
equal deleted inserted replaced
70794:da647a0c8313 70795:a90e40118874
    76         else if (limit == 0) {
    76         else if (limit == 0) {
    77           val requirements = dep_graph.all_preds(pending).reverse
    77           val requirements = dep_graph.all_preds(pending).reverse
    78           ((requirements, share_common_data), Load_Bulk(pending, Nil, checkpoints))
    78           ((requirements, share_common_data), Load_Bulk(pending, Nil, checkpoints))
    79         }
    79         }
    80         else {
    80         else {
    81           def count(node: Document.Node.Name): Int = if (finished(node)) 0 else 1
    81           val reachable = dep_graph.reachable_limit(limit, _ => 1, dep_graph.imm_preds, pending)
    82           val reachable = dep_graph.reachable_limit(limit, count _, dep_graph.imm_preds, pending)
       
    83           val (pending1, pending2) = pending.partition(reachable)
    82           val (pending1, pending2) = pending.partition(reachable)
    84           val requirements = dep_graph.all_preds(pending1).reverse
    83           val requirements = dep_graph.all_preds(pending1).reverse
    85           ((requirements, share_common_data), Load_Bulk(pending1, pending2, checkpoints))
    84           ((requirements, share_common_data), Load_Bulk(pending1, pending2, checkpoints))
    86         }
    85         }
    87       }
    86       }