# HG changeset patch
# User wenzelm
# Date 1570451038 -7200
# Node ID 9ee3558a7e99be773045300a66eac4f0ce8cf3bf
# Parent  28b50d6cc7cabd9a9aa12485b879ec008245e3d8
clarified Load_State / load_limit;

diff -r 28b50d6cc7ca -r 9ee3558a7e99 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Oct 07 13:58:18 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Oct 07 14:23:58 2019 +0200
@@ -44,12 +44,15 @@
       (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
   }
 
-  private val load_finished: (List[Document.Node.Name], Load_State) = (Nil, Load_State(Nil, Nil))
+  private object Load_State
+  {
+    def finished: Load_State = Load_State(Nil, Nil, 0)
+  }
 
-  private case class Load_State(pending: List[Document.Node.Name], rest: List[Document.Node.Name])
+  private case class Load_State(
+    pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Int)
   {
     def next(
-      limit: Int,
       dep_graph: Document.Node.Name.Graph[Unit],
       finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) =
     {
@@ -57,14 +60,14 @@
         : (List[Document.Node.Name], Load_State) =
       {
         val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished)
-        (load_theories, Load_State(pending1, rest1))
+        (load_theories, Load_State(pending1, rest1, load_limit))
       }
 
       if (!pending.forall(finished)) (Nil, this)
-      else if (rest.isEmpty) load_finished
-      else if (limit == 0) load_requirements(rest, Nil)
+      else if (rest.isEmpty) (Nil, Load_State.finished)
+      else if (load_limit == 0) load_requirements(rest, Nil)
       else {
-        val reachable = dep_graph.reachable_limit(limit, _ => 1, dep_graph.imm_preds, rest)
+        val reachable = dep_graph.reachable_limit(load_limit, _ => 1, dep_graph.imm_preds, rest)
         val (pending1, rest1) = rest.partition(reachable)
         load_requirements(pending1, rest1)
       }
@@ -94,12 +97,6 @@
     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 */
 
@@ -223,8 +220,7 @@
           }
           else result
 
-        val (load_theories, load_state1) =
-          load_state.next(load_limit, dep_graph, finished_theory(_))
+        val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory(_))
 
         (load_theories,
           copy(already_committed = already_committed1, result = result1, load_state = load_state1))
@@ -270,7 +266,8 @@
             val depth = dep_graph.node_depth(_ => 1)
             maximals.sortBy(node => - depth(node))
           }
-        val load_state = Load_State(Nil, rest)
+        val load_limit = if (commit.isDefined) session_options.int("headless_load_limit") else 0
+        val load_state = Load_State(Nil, rest, load_limit)
 
         Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit))
       }