src/Pure/Tools/build_process.scala

     def ok: Boolean = process_result.ok
   }
 
   object State {
     type Sessions = Map[String, Build_Job.Session_Context]
-    type Workers = List[Worker]
     type Pending = List[Task]
     type Running = Map[String, Job]
     type Results = Map[String, Result]
 
     def inc_serial(serial: Long): Long = {

   sealed case class State(
     serial: Long = 0,
     progress_seen: Long = 0,
     numa_next: Int = 0,
     sessions: State.Sessions = Map.empty,   // static build targets
-    workers: State.Workers = Nil,           // available worker processes
     pending: State.Pending = Nil,           // dynamic build "queue"
     running: State.Running = Map.empty,     // presently running jobs
     results: State.Results = Map.empty      // finished results
   ) {
     require(serial >= 0, "serial underflow")

     }
 
     def progress_serial(message_serial: Long = serial): State =
       if (message_serial > progress_seen) copy(progress_seen = message_serial)
       else error("Bad serial " + message_serial + " for progress output (already seen)")
-
-    def set_workers(new_workers: State.Workers): State = copy(workers = new_workers)
 
     def next_numa_node(numa_nodes: List[Int]): (Option[Int], State) =
       if (numa_nodes.isEmpty) (None, this)
       else {
         val available = numa_nodes.zipWithIndex

 
     def read_workers(
       db: SQL.Database,
       build_uuid: String = "",
       worker_uuid: String = ""
-    ): State.Workers = {
+    ): List[Worker] = {
       db.execute_query_statement(
         Workers.table.select(sql =
           SQL.where(Generic.sql(build_uuid = build_uuid, worker_uuid = worker_uuid))),
           List.from[Worker],
           { res =>

         val serial = serial_db max state.serial
         stamp_worker(db, worker_uuid, serial)
 
         val numa_next = Host.Data.read_numa_next(db, hostname)
         val sessions = pull1(read_sessions_domain(db), read_sessions(db, _), state.sessions)
-        val workers = read_workers(db)
         val pending = read_pending(db)
         val running = pull0(read_running(db), state.running)
         val results = pull1(read_results_domain(db), read_results(db, _), state.results)
 
         state.copy(serial = serial, numa_next = numa_next, sessions = sessions,
-          workers = workers, pending = pending, running = running, results = results)
+          pending = pending, running = running, results = results)
       }
     }
 
     def update_database(
       db: SQL.Database,

 
       val serial0 = state.serial
       val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0
 
       stamp_worker(db, worker_uuid, serial)
-      state.set_serial(serial).set_workers(read_workers(db))
+      state.set_serial(serial)
     }
   }
 }
 
 

     synchronized_database {
       _state = _state.inc_serial.progress_serial()
       for (db <- _database) {
         Build_Process.Data.write_progress(db, _state.serial, message, build_uuid)
         Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial)
-        _state = _state.set_workers(Build_Process.Data.read_workers(db))
       }
       build_progress_output
     }
   }
 

       val java_pid = java.pid
       val java_start = Date.instant(java.info.startInstant.get)
       _state = _state.inc_serial
       Build_Process.Data.start_worker(
         db, worker_uuid, build_uuid, hostname, java_pid, java_start, _state.serial)
-      _state = _state.set_workers(Build_Process.Data.read_workers(db))
     }
   }
 
   protected final def stop_worker(): Unit = synchronized_database {
     for (db <- _database) {
       Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop = true)
-      _state = _state.set_workers(Build_Process.Data.read_workers(db))
     }
   }
 
 
   /* run */