support headless_load_limit for more scalable load process;

--- a/etc/options	Mon Sep 30 13:23:49 2019 +0200
+++ b/etc/options	Mon Sep 30 16:40:35 2019 +0200
@@ -216,6 +216,9 @@
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
+option headless_load_limit : int = 0
+  -- "limit for loaded theories (0 = unlimited)"
+
 option execution_eager : bool = false
   -- "prefer theories with shorter stack of decendants"
 

--- a/src/Pure/General/graph.scala	Mon Sep 30 13:23:49 2019 +0200
+++ b/src/Pure/General/graph.scala	Mon Sep 30 16:40:35 2019 +0200
@@ -123,20 +123,25 @@
   def node_depth: Map[Key, Int] = reachable_length(imm_succs(_), minimals)
 
   /*reachable nodes with size limit*/
-  def reachable_limit(next: Key => Keys, limit: Int, xs: List[Key]): (List[Key], Keys) =
+  def reachable_limit(
+    limit: Int,
+    count: Key => Boolean,
+    next: Key => Keys,
+    xs: List[Key]): Keys =
   {
     def reach(res: (Int, Keys), x: Key): (Int, Keys) =
     {
       val (n, rs) = res
-      if (rs.contains(x)) res else ((n + 1, rs + x) /: next(x))(reach _)
+      if (rs.contains(x)) res
+      else ((if (count(x)) n + 1 else n, rs + x) /: next(x))(reach _)
     }
 
-    @tailrec def reachs(size: Int, rs: Keys, rest: List[Key]): (List[Key], Keys) =
+    @tailrec def reachs(size: Int, rs: Keys, rest: List[Key]): Keys =
       rest match {
-        case Nil => (rest, rs)
+        case Nil => rs
         case head :: tail =>
           val (size1, rs1) = reach((size, rs), head)
-          if (size > 0 && size1 > limit) (rest, rs)
+          if (size > 0 && size1 > limit) rs
           else reachs(size1, rs1, tail)
       }
 

--- a/src/Pure/PIDE/headless.scala	Mon Sep 30 13:23:49 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 30 16:40:35 2019 +0200
@@ -48,26 +48,45 @@
   {
     type Result = (List[Document.Node.Name], Load_State)
 
-    def next(dep_graph: Document.Node.Name.Graph[Unit], finished: Document.Node.Name => Boolean)
-      : Result =
+    def next(
+      limit: Int,
+      dep_graph: Document.Node.Name.Graph[Unit],
+      finished: Document.Node.Name => Boolean): Result =
     {
+      def make_pending(maximals: List[Document.Node.Name]): List[Document.Node.Name] =
+      {
+        val pending = maximals.filterNot(finished)
+        if (pending.isEmpty || pending.tail.isEmpty) pending
+        else {
+          val depth = dep_graph.node_depth
+          pending.sortBy(node => - depth(node))
+        }
+      }
+
       def load_checkpoints(checkpoints: List[Document.Node.Name]): Result =
-        Load_Init(checkpoints).next(dep_graph, finished)
+        Load_Init(checkpoints).next(limit, dep_graph, finished)
 
       def load_requirements(
         pending: List[Document.Node.Name], checkpoints: List[Document.Node.Name]): Result =
       {
-        if (pending.nonEmpty) {
+        if (pending.isEmpty) load_checkpoints(checkpoints)
+        else if (limit == 0) {
           val requirements = dep_graph.all_preds(pending).reverse
-          (requirements, Load_Bulk(pending, checkpoints))
+          (requirements, Load_Bulk(pending, Nil, checkpoints))
         }
-        else load_checkpoints(checkpoints)
+        else {
+          def count(node: Document.Node.Name): Boolean = !finished(node)
+          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
+          (requirements, Load_Bulk(pending1, pending2, checkpoints))
+        }
       }
 
       val (load_theories, st1) =
         this match {
           case Load_Init(Nil) =>
-            val pending = dep_graph.maximals.filterNot(finished)
+            val pending = make_pending(dep_graph.maximals)
             if (pending.isEmpty) (Nil, Load_Finished) else load_requirements(pending, Nil)
           case Load_Init(target :: checkpoints) =>
             (dep_graph.all_preds(List(target)).reverse, Load_Target(target, checkpoints))
@@ -77,11 +96,10 @@
               else dep_graph.exclude(dep_graph.all_succs(checkpoints).toSet)
             val dep_graph2 =
               dep_graph1.restrict(dep_graph.all_succs(List(pending)).toSet)
-            val pending2 =
-              dep_graph.maximals.filter(node => dep_graph2.defined(node) && !finished(node))
+            val pending2 = make_pending(dep_graph.maximals.filter(dep_graph2.defined))
             load_requirements(pending2, checkpoints)
-          case Load_Bulk(pending, checkpoints) if pending.forall(finished) =>
-            load_checkpoints(checkpoints)
+          case Load_Bulk(pending, remaining, checkpoints) if pending.forall(finished) =>
+            load_requirements(remaining, checkpoints)
           case st => (Nil, st)
         }
       (load_theories.filterNot(finished), st1)
@@ -91,7 +109,9 @@
   private case class Load_Target(
     pending: Document.Node.Name, checkpoints: List[Document.Node.Name]) extends Load_State
   private case class Load_Bulk(
-    pending: List[Document.Node.Name], checkpoints: List[Document.Node.Name]) extends Load_State
+    pending: List[Document.Node.Name],
+    remaining: List[Document.Node.Name],
+    checkpoints: List[Document.Node.Name]) extends Load_State
   private case object Load_Finished extends Load_State
 
   class Session private[Headless](
@@ -114,6 +134,12 @@
     def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
     def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
 
+    def load_limit: Int =
+    {
+      val limit = session_options.int("headless_load_limit")
+      if (limit == 0) Integer.MAX_VALUE else limit
+    }
+
 
     /* temporary directory */
 
@@ -237,7 +263,8 @@
           }
           else result
 
-        val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory(_))
+        val (load_theories, load_state1) =
+          load_state.next(load_limit, dep_graph, finished_theory(_))
 
         (load_theories,
           copy(already_committed = already_committed1, result = result1, load_state = load_state1))