# HG changeset patch
# User wenzelm
# Date 1677607951 -3600
# Node ID 6b928419f109279a2b493b93c1fb06e81eeb482a
# Parent  0d5994eef9e6c154de75b4580b7096ddce77f684
clarified signature: allow more general init, e.g. from existing database;

diff -r 0d5994eef9e6 -r 6b928419f109 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 28 17:42:13 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 28 19:12:31 2023 +0100
@@ -513,12 +513,18 @@
   def close(): Unit = database.foreach(_.close())
 
   // global state
-  protected var _state: Build_Process.State = init_state()
+  protected var _state: Build_Process.State = init_state(Build_Process.State())
 
-  protected def init_state(): Build_Process.State =
-    Build_Process.State(pending =
-      (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
-        yield Build_Process.Entry(name, preds.toList)).toList)
+  protected def init_state(state: Build_Process.State): Build_Process.State = {
+    val old_pending = state.pending.iterator.map(_.name).toSet
+    val new_pending =
+      List.from(
+        for {
+          (name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator
+          if !old_pending(name)
+        } yield Build_Process.Entry(name, preds.toList))
+    state.copy(pending = new_pending ::: state.pending)
+  }
 
   protected def next_pending(): Option[String] = synchronized {
     if (_state.running.size < (build_context.max_jobs max 1)) {