diff -r 2beac4adc565 -r 7c77fb7a6fc9 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Oct 14 22:22:06 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Oct 14 22:34:33 2019 +0200
@@ -44,40 +44,6 @@
       (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
   }
 
-  private object Load_State
-  {
-    def finished: Load_State = Load_State(Nil, Nil, 0)
-
-    def count_file(name: Document.Node.Name): Long =
-      name.path.file.length
-  }
-
-  private case class Load_State(
-    pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long)
-  {
-    def next(
-      dep_graph: Document.Node.Name.Graph[Unit],
-      finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) =
-    {
-      def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name])
-        : (List[Document.Node.Name], Load_State) =
-      {
-        val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished)
-        (load_theories, Load_State(pending1, rest1, load_limit))
-      }
-
-      if (!pending.forall(finished)) (Nil, this)
-      else if (rest.isEmpty) (Nil, Load_State.finished)
-      else if (load_limit == 0) load_requirements(rest, Nil)
-      else {
-        val reachable =
-          dep_graph.reachable_limit(load_limit, Load_State.count_file, dep_graph.imm_preds, rest)
-        val (pending1, rest1) = rest.partition(reachable)
-        load_requirements(pending1, rest1)
-      }
-    }
-  }
-
   class Session private[Headless](
     session_name: String,
     _session_options: => Options,
@@ -121,6 +87,40 @@
 
     /* theories */
 
+    private object Load_State
+    {
+      def finished: Load_State = Load_State(Nil, Nil, 0)
+
+      def count_file(name: Document.Node.Name): Long =
+        name.path.file.length
+    }
+
+    private case class Load_State(
+      pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long)
+    {
+      def next(
+        dep_graph: Document.Node.Name.Graph[Unit],
+        finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) =
+      {
+        def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name])
+          : (List[Document.Node.Name], Load_State) =
+        {
+          val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished)
+          (load_theories, Load_State(pending1, rest1, load_limit))
+        }
+
+        if (!pending.forall(finished)) (Nil, this)
+        else if (rest.isEmpty) (Nil, Load_State.finished)
+        else if (load_limit == 0) load_requirements(rest, Nil)
+        else {
+          val reachable =
+            dep_graph.reachable_limit(load_limit, Load_State.count_file, dep_graph.imm_preds, rest)
+          val (pending1, rest1) = rest.partition(reachable)
+          load_requirements(pending1, rest1)
+        }
+      }
+    }
+
     private sealed case class Use_Theories_State(
       dep_graph: Document.Node.Name.Graph[Unit],
       load_state: Load_State,