# HG changeset patch
# User wenzelm
# Date 1678092401 -3600
# Node ID 3481e54bd8f12cad684d7cb1dd8253dc15bc60df
# Parent  3362f84a300afbb856ca5d17d7782a457cace5b1
tuned comments;
tuned structure;

diff -r 3362f84a300a -r 3481e54bd8f1 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 06 09:37:02 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 06 09:46:41 2023 +0100
@@ -264,26 +264,8 @@
       val table = make_table("", List(build_uuid, ml_platform, options))
     }
 
-    object Workers {
-      val worker_uuid = Generic.worker_uuid.make_primary_key
-      val build_uuid = Generic.build_uuid
-      val stamp = SQL.Column.date("stamp")
-      val serial = SQL.Column.long("serial")
 
-      val table = make_table("workers", List(worker_uuid, build_uuid, stamp, serial))
-
-      val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
-    }
-
-    object Progress {
-      val serial = SQL.Column.long("serial").make_primary_key
-      val kind = SQL.Column.int("kind")
-      val text = SQL.Column.string("text")
-      val verbose = SQL.Column.bool("verbose")
-      val build_uuid = Generic.build_uuid
-
-      val table = make_table("progress", List(serial, kind, text, verbose, build_uuid))
-    }
+    /* sessions */
 
     object Sessions {
       val name = Generic.name.make_primary_key
@@ -299,93 +281,6 @@
         List(name, deps, ancestors, sources, timeout, old_time, old_command_timings, build_uuid))
     }
 
-    object Pending {
-      val name = Generic.name.make_primary_key
-      val deps = SQL.Column.string("deps")
-      val info = SQL.Column.string("info")
-
-      val table = make_table("pending", List(name, deps, info))
-    }
-
-    object Running {
-      val name = Generic.name.make_primary_key
-      val hostname = SQL.Column.string("hostname")
-      val numa_node = SQL.Column.int("numa_node")
-
-      val table = make_table("running", List(name, hostname, numa_node))
-    }
-
-    object Results {
-      val name = Generic.name.make_primary_key
-      val hostname = SQL.Column.string("hostname")
-      val numa_node = SQL.Column.string("numa_node")
-      val rc = SQL.Column.int("rc")
-      val out = SQL.Column.string("out")
-      val err = SQL.Column.string("err")
-      val timing_elapsed = SQL.Column.long("timing_elapsed")
-      val timing_cpu = SQL.Column.long("timing_cpu")
-      val timing_gc = SQL.Column.long("timing_gc")
-
-      val table =
-        make_table("results",
-          List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc))
-    }
-
-    def get_serial(db: SQL.Database, worker_uuid: String = ""): Long =
-      db.using_statement(
-        Workers.table.select(List(Workers.serial_max),
-          sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
-      )(stmt => stmt.execute_query().iterator(_.long(Workers.serial)).nextOption.getOrElse(0L))
-
-    def set_serial(db: SQL.Database, worker_uuid: String, build_uuid: String, serial: Long): Unit = {
-      if (get_serial(db, worker_uuid = worker_uuid) != serial) {
-        db.using_statement(
-          Workers.table.delete(sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
-        )(_.execute())
-        db.using_statement(Workers.table.insert()) { stmt =>
-          stmt.string(1) = worker_uuid
-          stmt.string(2) = build_uuid
-          stmt.date(3) = db.now()
-          stmt.long(4) = serial
-          stmt.execute()
-        }
-      }
-    }
-
-    def read_progress(db: SQL.Database, seen: Long = 0, build_uuid: String = ""): Progress_Messages =
-      db.using_statement(
-        Progress.table.select(
-          sql =
-            SQL.where(
-              SQL.and(
-                if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
-                Generic.sql(build_uuid = build_uuid))))
-      ) { stmt =>
-          SortedMap.from(stmt.execute_query().iterator { res =>
-            val serial = res.long(Progress.serial)
-            val kind = isabelle.Progress.Kind(res.int(Progress.kind))
-            val text = res.string(Progress.text)
-            val verbose = res.bool(Progress.verbose)
-            serial -> isabelle.Progress.Message(kind, text, verbose = verbose)
-          })
-        }
-
-    def write_progress(
-      db: SQL.Database,
-      message_serial: Long,
-      message: isabelle.Progress.Message,
-      build_uuid: String
-    ): Unit = {
-      db.using_statement(Progress.table.insert()) { stmt =>
-        stmt.long(1) = message_serial
-        stmt.int(2) = message.kind.id
-        stmt.string(3) = message.text
-        stmt.bool(4) = message.verbose
-        stmt.string(5) = build_uuid
-        stmt.execute()
-      }
-    }
-
     def read_sessions_domain(db: SQL.Database): Set[String] =
       db.using_statement(Sessions.table.select(List(Sessions.name)))(stmt =>
         Set.from(stmt.execute_query().iterator(_.string(Sessions.name))))
@@ -429,6 +324,99 @@
       insert.nonEmpty
     }
 
+
+    /* progress */
+
+    object Progress {
+      val serial = SQL.Column.long("serial").make_primary_key
+      val kind = SQL.Column.int("kind")
+      val text = SQL.Column.string("text")
+      val verbose = SQL.Column.bool("verbose")
+      val build_uuid = Generic.build_uuid
+
+      val table = make_table("progress", List(serial, kind, text, verbose, build_uuid))
+    }
+
+    def read_progress(db: SQL.Database, seen: Long = 0, build_uuid: String = ""): Progress_Messages =
+      db.using_statement(
+        Progress.table.select(
+          sql =
+            SQL.where(
+              SQL.and(
+                if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
+                Generic.sql(build_uuid = build_uuid))))
+      ) { stmt =>
+          SortedMap.from(stmt.execute_query().iterator { res =>
+            val serial = res.long(Progress.serial)
+            val kind = isabelle.Progress.Kind(res.int(Progress.kind))
+            val text = res.string(Progress.text)
+            val verbose = res.bool(Progress.verbose)
+            serial -> isabelle.Progress.Message(kind, text, verbose = verbose)
+          })
+        }
+
+    def write_progress(
+      db: SQL.Database,
+      message_serial: Long,
+      message: isabelle.Progress.Message,
+      build_uuid: String
+    ): Unit = {
+      db.using_statement(Progress.table.insert()) { stmt =>
+        stmt.long(1) = message_serial
+        stmt.int(2) = message.kind.id
+        stmt.string(3) = message.text
+        stmt.bool(4) = message.verbose
+        stmt.string(5) = build_uuid
+        stmt.execute()
+      }
+    }
+
+
+    /* workers */
+
+    object Workers {
+      val worker_uuid = Generic.worker_uuid.make_primary_key
+      val build_uuid = Generic.build_uuid
+      val stamp = SQL.Column.date("stamp")
+      val serial = SQL.Column.long("serial")
+
+      val table = make_table("workers", List(worker_uuid, build_uuid, stamp, serial))
+
+      val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
+    }
+
+    def get_serial(db: SQL.Database, worker_uuid: String = ""): Long =
+      db.using_statement(
+        Workers.table.select(List(Workers.serial_max),
+          sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
+      )(stmt => stmt.execute_query().iterator(_.long(Workers.serial)).nextOption.getOrElse(0L))
+
+    def set_serial(db: SQL.Database, worker_uuid: String, build_uuid: String, serial: Long): Unit = {
+      if (get_serial(db, worker_uuid = worker_uuid) != serial) {
+        db.using_statement(
+          Workers.table.delete(sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
+        )(_.execute())
+        db.using_statement(Workers.table.insert()) { stmt =>
+          stmt.string(1) = worker_uuid
+          stmt.string(2) = build_uuid
+          stmt.date(3) = db.now()
+          stmt.long(4) = serial
+          stmt.execute()
+        }
+      }
+    }
+
+
+    /* pending jobs */
+
+    object Pending {
+      val name = Generic.name.make_primary_key
+      val deps = SQL.Column.string("deps")
+      val info = SQL.Column.string("info")
+
+      val table = make_table("pending", List(name, deps, info))
+    }
+
     def read_pending(db: SQL.Database): List[Entry] =
       db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt =>
         List.from(
@@ -462,6 +450,17 @@
       delete.nonEmpty || insert.nonEmpty
     }
 
+
+    /* running jobs */
+
+    object Running {
+      val name = Generic.name.make_primary_key
+      val hostname = SQL.Column.string("hostname")
+      val numa_node = SQL.Column.int("numa_node")
+
+      val table = make_table("running", List(name, hostname, numa_node))
+    }
+
     def read_running(db: SQL.Database): List[Build_Job.Abstract] =
       db.using_statement(Running.table.select(sql = SQL.order_by(List(Running.name)))) { stmt =>
         List.from(
@@ -497,6 +496,25 @@
       delete.nonEmpty || insert.nonEmpty
     }
 
+
+    /* job results */
+
+    object Results {
+      val name = Generic.name.make_primary_key
+      val hostname = SQL.Column.string("hostname")
+      val numa_node = SQL.Column.string("numa_node")
+      val rc = SQL.Column.int("rc")
+      val out = SQL.Column.string("out")
+      val err = SQL.Column.string("err")
+      val timing_elapsed = SQL.Column.long("timing_elapsed")
+      val timing_cpu = SQL.Column.long("timing_cpu")
+      val timing_gc = SQL.Column.long("timing_gc")
+
+      val table =
+        make_table("results",
+          List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc))
+    }
+
     def read_results_domain(db: SQL.Database): Set[String] =
       db.using_statement(Results.table.select(List(Results.name)))(stmt =>
         Set.from(stmt.execute_query().iterator(_.string(Results.name))))
@@ -551,6 +569,9 @@
       insert.nonEmpty
     }
 
+
+    /* collective operations */
+
     def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
       val tables =
         List(