# HG changeset patch
# User wenzelm
# Date 1678285555 -3600
# Node ID 80021d645a01699ef141b763bacb9a28326cf0da
# Parent  89c42ec77a844cde3d0c570c9f0a93ebfe61aa39
tuned structure;

diff -r 89c42ec77a84 -r 80021d645a01 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 15:22:57 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 15:25:55 2023 +0100
@@ -465,6 +465,29 @@
       val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
     }
 
+    def read_workers(
+      db: SQL.Database,
+      build_uuid: String = "",
+      worker_uuid: String = ""
+    ): State.Workers = {
+      db.execute_query_statement(
+        Workers.table.select(sql =
+          SQL.where(Generic.sql(build_uuid = build_uuid, worker_uuid = worker_uuid))),
+          List.from[Worker],
+          { res =>
+            Worker(
+              worker_uuid = res.string(Workers.worker_uuid),
+              build_uuid = res.string(Workers.build_uuid),
+              hostname = res.string(Workers.hostname),
+              java_pid = res.long(Workers.java_pid),
+              java_start = res.get_date(Workers.java_start),
+              start = res.date(Workers.start),
+              stamp = res.date(Workers.stamp),
+              stop = res.get_date(Workers.stop),
+              serial = res.long(Workers.serial))
+          })
+    }
+
     def serial_max(db: SQL.Database): Long =
       db.execute_query_statementO[Long](
         Workers.table.select(List(Workers.serial_max)),
@@ -529,29 +552,6 @@
         })
     }
 
-    def read_workers(
-      db: SQL.Database,
-      build_uuid: String = "",
-      worker_uuid: String = ""
-    ): State.Workers = {
-      db.execute_query_statement(
-        Workers.table.select(sql =
-          SQL.where(Generic.sql(build_uuid = build_uuid, worker_uuid = worker_uuid))),
-          List.from[Worker],
-          { res =>
-            Worker(
-              worker_uuid = res.string(Workers.worker_uuid),
-              build_uuid = res.string(Workers.build_uuid),
-              hostname = res.string(Workers.hostname),
-              java_pid = res.long(Workers.java_pid),
-              java_start = res.get_date(Workers.java_start),
-              start = res.date(Workers.start),
-              stamp = res.date(Workers.stamp),
-              stop = res.get_date(Workers.stop),
-              serial = res.long(Workers.serial))
-          })
-    }
-
 
     /* pending jobs */