# HG changeset patch
# User wenzelm
# Date 1677673429 -3600
# Node ID dcbf96acae274aeabdecd064f6ac8c73cd9e36c9
# Parent  c10fa027caa06dadbff1ad1723476e03596bf810
clarified signature: do not expose global state to object-oriented variants;

diff -r c10fa027caa0 -r dcbf96acae27 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 11:30:54 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 13:23:49 2023 +0100
@@ -529,9 +529,11 @@
     }
 
 
-  /* database */
+  /* global state: internal var vs. external database */
 
-  protected val database: Option[SQL.Database] =
+  private var _state: Build_Process.State = init_state(Build_Process.State())
+
+  private val _database: Option[SQL.Database] =
     if (!build_options.bool("build_database_test")) None
     else if (store.database_server) Some(store.open_database_server())
     else {
@@ -541,10 +543,8 @@
       Some(db)
     }
 
-  def close(): Unit = database.foreach(_.close())
-
-  protected def setup_database(): Unit =
-    for (db <- database) {
+  private def setup_database(): Unit =
+    for (db <- _database) {
       synchronized {
         db.transaction {
           Build_Process.Data.init_database(db, build_context)
@@ -552,8 +552,9 @@
       }
       db.rebuild()
     }
-  protected def sync_database(): Unit =
-    for (db <- database) {
+
+  private def sync_database(): Unit =
+    for (db <- _database) {
       synchronized {
         db.transaction {
           _state =
@@ -563,10 +564,10 @@
       }
     }
 
+  def close(): Unit = _database.foreach(_.close())
 
-  /* global state */
 
-  protected var _state: Build_Process.State = init_state(Build_Process.State())
+  /* policy operations */
 
   protected def init_state(state: Build_Process.State): Build_Process.State = {
     val old_pending = state.pending.iterator.map(_.name).toSet
@@ -579,14 +580,13 @@
     state.copy(pending = new_pending ::: state.pending)
   }
 
-  protected def next_pending(): Option[String] = synchronized {
-    if (_state.running.size < (build_context.max_jobs max 1)) {
-      _state.pending.filter(entry => entry.is_ready && !_state.is_running(entry.name))
+  protected def next_job(state: Build_Process.State): Option[String] =
+    if (state.running.size < (build_context.max_jobs max 1)) {
+      state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
         .sortBy(_.name)(build_context.ordering)
         .headOption.map(_.name)
     }
     else None
-  }
 
   protected def start_job(session_name: String): Unit = {
     val ancestor_results = synchronized {
@@ -681,14 +681,14 @@
 
   /* run */
 
-  protected def sleep(): Unit =
-    Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
-      build_options.seconds("editor_input_delay").sleep()
-    }
-
   def run(): Map[String, Process_Result] = {
     def finished(): Boolean = synchronized { _state.finished }
 
+    def sleep(): Unit =
+      Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
+        build_options.seconds("editor_input_delay").sleep()
+      }
+
     if (finished()) {
       progress.echo_warning("Nothing to build")
       Map.empty[String, Process_Result]
@@ -709,7 +709,7 @@
           }
         }
 
-        next_pending() match {
+        synchronized { next_job(_state) } match {
           case Some(name) =>
             start_job(name)
           case None =>