more database content, e.g. for monitoring;

--- a/src/Pure/Tools/build_job.scala	Wed Mar 08 15:25:55 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 08 15:50:29 2023 +0100
@@ -12,11 +12,12 @@
 
 trait Build_Job {
   def job_name: String
+  def worker_uuid: String
   def node_info: Host.Node_Info
   def cancel(): Unit = ()
   def is_finished: Boolean = false
   def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
-  def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info)
+  def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, worker_uuid, node_info)
 }
 
 object Build_Job {
@@ -26,6 +27,7 @@
 
   sealed case class Abstract(
     override val job_name: String,
+    override val worker_uuid: String,
     override val node_info: Host.Node_Info
   ) extends Build_Job {
     override def make_abstract: Abstract = this
@@ -38,13 +40,15 @@
 
   def start_session(
     build_context: Build_Process.Context,
+    worker_uuid: String,
     progress: Progress,
     log: Logger,
     session_background: Sessions.Background,
     input_shasum: SHA1.Shasum,
     node_info: Host.Node_Info
   ): Session_Job = {
-    new Session_Job(build_context, progress, log, session_background, input_shasum, node_info)
+    new Session_Job(
+      build_context, worker_uuid, progress, log, session_background, input_shasum, node_info)
   }
 
   object Session_Context {
@@ -106,6 +110,7 @@
 
   class Session_Job private[Build_Job](
     build_context: Build_Process.Context,
+    override val worker_uuid: String,
     progress: Progress,
     log: Logger,
     session_background: Sessions.Background,

--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 15:25:55 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 15:50:29 2023 +0100
@@ -600,10 +600,11 @@
 
     object Running {
       val name = Generic.name.make_primary_key
+      val worker_uuid = Generic.worker_uuid
       val hostname = SQL.Column.string("hostname")
       val numa_node = SQL.Column.int("numa_node")
 
-      val table = make_table("running", List(name, hostname, numa_node))
+      val table = make_table("running", List(name, worker_uuid, hostname, numa_node))
     }
 
     def read_running(db: SQL.Database): List[Build_Job.Abstract] =
@@ -612,9 +613,10 @@
         List.from[Build_Job.Abstract],
         { res =>
           val name = res.string(Running.name)
+          val worker_uuid = res.string(Running.worker_uuid)
           val hostname = res.string(Running.hostname)
           val numa_node = res.get_int(Running.numa_node)
-          Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node))
+          Build_Job.Abstract(name, worker_uuid, Host.Node_Info(hostname, numa_node))
         }
       )
 
@@ -633,8 +635,9 @@
         db.execute_statement(Running.table.insert(), body =
           { stmt =>
             stmt.string(1) = job.job_name
-            stmt.string(2) = job.node_info.hostname
-            stmt.int(3) = job.node_info.numa_node
+            stmt.string(2) = job.worker_uuid
+            stmt.string(3) = job.node_info.hostname
+            stmt.int(4) = job.node_info.numa_node
           })
       }
 
@@ -908,7 +911,7 @@
       store.init_output(session_name)
 
       val job =
-        Build_Job.start_session(build_context, progress, log,
+        Build_Job.start_session(build_context, worker_uuid, progress, log,
           build_deps.background(session_name), input_shasum, node_info)
       state1.add_running(session_name, job)
     }