# HG changeset patch
# User wenzelm
# Date 1570461626 -7200
# Node ID 44eeca528557277640210f625559264ea6c089e9
# Parent  f8cd5f0f2b613ff73732243acb3a5292eff8aac1
count document nodes via raw file length;

diff -r f8cd5f0f2b61 -r 44eeca528557 etc/options
--- a/etc/options	Mon Oct 07 15:04:18 2019 +0200
+++ b/etc/options	Mon Oct 07 17:20:26 2019 +0200
@@ -222,8 +222,8 @@
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
-option headless_load_limit : int = 100
-  -- "limit for loaded theories (0 = unlimited)"
+option headless_load_limit : int = 5
+  -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
 section "Miscellaneous Tools"
diff -r f8cd5f0f2b61 -r 44eeca528557 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Mon Oct 07 15:04:18 2019 +0200
+++ b/src/Pure/General/graph.scala	Mon Oct 07 17:20:26 2019 +0200
@@ -113,35 +113,35 @@
 
   /*reachable nodes with length of longest path*/
   def reachable_length(
-    count: Key => Int,
+    count: Key => Long,
     next: Key => Keys,
-    xs: List[Key]): Map[Key, Int] =
+    xs: List[Key]): Map[Key, Long] =
   {
-    def reach(length: Int)(rs: Map[Key, Int], x: Key): Map[Key, Int] =
+    def reach(length: Long)(rs: Map[Key, Long], x: Key): Map[Key, Long] =
       if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs
       else ((rs + (x -> length)) /: next(x))(reach(length + count(x)))
-    (Map.empty[Key, Int] /: xs)(reach(0))
+    (Map.empty[Key, Long] /: xs)(reach(0))
   }
-  def node_height(count: Key => Int): Map[Key, Int] =
+  def node_height(count: Key => Long): Map[Key, Long] =
     reachable_length(count, imm_preds(_), maximals)
-  def node_depth(count: Key => Int): Map[Key, Int] =
+  def node_depth(count: Key => Long): Map[Key, Long] =
     reachable_length(count, imm_succs(_), minimals)
 
   /*reachable nodes with size limit*/
   def reachable_limit(
-    limit: Int,
-    count: Key => Int,
+    limit: Long,
+    count: Key => Long,
     next: Key => Keys,
     xs: List[Key]): Keys =
   {
-    def reach(res: (Int, Keys), x: Key): (Int, Keys) =
+    def reach(res: (Long, Keys), x: Key): (Long, Keys) =
     {
       val (n, rs) = res
       if (rs.contains(x)) res
       else ((n + count(x), rs + x) /: next(x))(reach _)
     }
 
-    @tailrec def reachs(size: Int, rs: Keys, rest: List[Key]): Keys =
+    @tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys =
       rest match {
         case Nil => rs
         case head :: tail =>
diff -r f8cd5f0f2b61 -r 44eeca528557 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Oct 07 15:04:18 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Oct 07 17:20:26 2019 +0200
@@ -47,10 +47,13 @@
   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: Int)
+    pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long)
   {
     def next(
       dep_graph: Document.Node.Name.Graph[Unit],
@@ -67,7 +70,8 @@
       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, _ => 1, dep_graph.imm_preds, rest)
+        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)
       }
@@ -263,10 +267,12 @@
         val rest =
           if (maximals.isEmpty || maximals.tail.isEmpty) maximals
           else {
-            val depth = dep_graph.node_depth(_ => 1)
+            val depth = dep_graph.node_depth(Load_State.count_file)
             maximals.sortBy(node => - depth(node))
           }
-        val load_limit = if (commit.isDefined) session_options.int("headless_load_limit") else 0
+        val load_limit =
+          if (commit.isDefined) session_options.int("headless_load_limit").toLong * 1024 * 1024
+          else 0
         val load_state = Load_State(Nil, rest, load_limit)
 
         Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit))