more informative Build_Process.Snapshot;
authorwenzelm
Tue, 14 Mar 2023 19:41:16 +0100
changeset 77660 57fdb6c846b0
parent 77659 d7eb6a4522b8
child 77661 45bd5c26cbcc
more informative Build_Process.Snapshot;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 19:19:38 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 19:41:16 2023 +0100
@@ -145,6 +145,15 @@
   type Progress_Messages = SortedMap[Long, Progress.Message]
   val progress_messages_empty: Progress_Messages = SortedMap.empty
 
+  case class Build(
+    build_uuid: String,
+    ml_platform: String,
+    options: String,
+    start: Date,
+    stop: Option[Date],
+    progress_stopped: Boolean
+  )
+
   case class Worker(
     worker_uuid: String,
     build_uuid: String,
@@ -191,6 +200,7 @@
 
   sealed case class Snapshot(
     progress_messages: Progress_Messages,
+    builds: List[Build],        // available build configurations
     workers: List[Worker],      // available worker processes
     sessions: State.Sessions,   // static build targets
     pending: State.Pending,     // dynamic build "queue"
@@ -348,6 +358,20 @@
         make_table("", List(build_uuid, ml_platform, options, start, stop, progress_stopped))
     }
 
+    def read_builds(db: SQL.Database, build_uuid: String = ""): List[Build] =
+      db.execute_query_statement(
+        Base.table.select(sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+        List.from[Build],
+        { res =>
+          val build_uuid = res.string(Base.build_uuid)
+          val ml_platform = res.string(Base.ml_platform)
+          val options = res.string(Base.options)
+          val start = res.date(Base.start)
+          val stop = res.get_date(Base.stop)
+          val progress_stopped = res.bool(Base.progress_stopped)
+          Build(build_uuid, ml_platform, options, start, stop, progress_stopped)
+        })
+
     def start_build(
       db: SQL.Database,
       build_uuid: String,
@@ -1174,15 +1198,17 @@
   /* snapshot */
 
   def snapshot(): Build_Process.Snapshot = synchronized_database {
-    val (progress_messages, workers) =
+    val (progress_messages, builds, workers) =
       _database match {
-        case None => (Build_Process.progress_messages_empty, Nil)
+        case None => (Build_Process.progress_messages_empty, Nil, Nil)
         case Some(db) =>
           (Build_Process.Data.read_progress(db),
+           Build_Process.Data.read_builds(db),
            Build_Process.Data.read_workers(db))
       }
     Build_Process.Snapshot(
       progress_messages = progress_messages,
+      builds = builds,
       workers = workers,
       sessions = _state.sessions,
       pending = _state.pending,