# HG changeset patch
# User wenzelm
# Date 1687774048 -7200
# Node ID 928ef137758cb936b8fd86949272a819a2975402
# Parent  c268def0784bf209eec3acc5b8e22154f8f66655
tuned signature;

diff -r c268def0784b -r 928ef137758c src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Jun 23 14:43:15 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Mon Jun 26 12:07:28 2023 +0200
@@ -802,14 +802,14 @@
 
   /* progress backed by database */
 
-  private val _database: Option[SQL.Database] =
+  private val _build_database: Option[SQL.Database] =
     store.maybe_open_build_database(Build_Process.Data.database)
 
   private val _host_database: Option[SQL.Database] =
     store.maybe_open_build_database(Host.Data.database)
 
   protected val (progress, worker_uuid) = synchronized {
-    _database match {
+    _build_database match {
       case None => (build_progress, UUID.random().toString)
       case Some(db) =>
         val progress_db = store.open_build_database(Progress.Data.database)
@@ -824,7 +824,7 @@
   protected val log: Logger = Logger.make_system_log(progress, build_options)
 
   def close(): Unit = synchronized {
-    _database.foreach(_.close())
+    _build_database.foreach(_.close())
     _host_database.foreach(_.close())
     progress match {
       case db_progress: Database_Progress =>
@@ -839,7 +839,7 @@
   private var _state: Build_Process.State = Build_Process.State()
 
   protected def synchronized_database[A](body: => A): A = synchronized {
-    _database match {
+    _build_database match {
       case None => body
       case Some(db) =>
         Build_Process.Data.transaction_lock(db) {
@@ -964,27 +964,27 @@
     !Long_Name.is_qualified(job_name)
 
   protected final def start_build(): Unit = synchronized_database {
-    for (db <- _database) {
+    for (db <- _build_database) {
       Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
         build_context.sessions_structure.session_prefs)
     }
   }
 
   protected final def stop_build(): Unit = synchronized_database {
-    for (db <- _database) {
+    for (db <- _build_database) {
       Build_Process.Data.stop_build(db, build_uuid)
     }
   }
 
   protected final def start_worker(): Unit = synchronized_database {
-    for (db <- _database) {
+    for (db <- _build_database) {
       _state = _state.inc_serial
       Build_Process.Data.start_worker(db, worker_uuid, build_uuid, _state.serial)
     }
   }
 
   protected final def stop_worker(): Unit = synchronized_database {
-    for (db <- _database) {
+    for (db <- _build_database) {
       Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop = true)
     }
   }
@@ -1060,7 +1060,7 @@
 
   def snapshot(): Build_Process.Snapshot = synchronized_database {
     val (builds, workers) =
-      _database match {
+      _build_database match {
         case None => (Nil, Nil)
         case Some(db) =>
           (Build_Process.Data.read_builds(db),