# HG changeset patch
# User wenzelm
# Date 1687948783 -7200
# Node ID 73be8ec887219b620db7a77dad3734590e571a44
# Parent  5da972859ea6041454ce30f8be845da6ccc3b9a7
clarified signature: more concise data;

diff -r 5da972859ea6 -r 73be8ec88721 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jun 28 12:30:30 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jun 28 12:39:43 2023 +0200
@@ -432,15 +432,9 @@
     val store = build_init(options, cache = cache)
     val build_options = store.options
 
-    val sessions =
-      using_optional(store.maybe_open_build_database()) {
-        case None => error("Cannot access build database")
-        case Some(db) => Build_Process.read_sessions(db, build_master.build_uuid)
-      }
-
     val sessions_structure =
       Sessions.load_structure(build_options, dirs = dirs).
-        selection(Sessions.Selection(sessions = sessions))
+        selection(Sessions.Selection(sessions = build_master.sessions))
 
     val build_deps =
       Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors
diff -r 5da972859ea6 -r 73be8ec88721 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Jun 28 12:30:30 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jun 28 12:39:43 2023 +0200
@@ -147,7 +147,8 @@
     ml_platform: String,
     options: String,
     start: Date,
-    stop: Option[Date]
+    stop: Option[Date],
+    sessions: List[String]
   ) {
     def active: Boolean = stop.isEmpty
   }
@@ -334,18 +335,25 @@
       val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
     }
 
-    def read_builds(db: SQL.Database, build_uuid: String = ""): List[Build] =
-      db.execute_query_statement(
-        Base.table.select(sql = Generic.sql_where(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)
-          Build(build_uuid, ml_platform, options, start, stop)
-        }).sortBy(_.start)(Date.Ordering)
+    def read_builds(db: SQL.Database, build_uuid: String = ""): List[Build] = {
+      val builds =
+        db.execute_query_statement(
+          Base.table.select(sql = Generic.sql_where(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)
+            Build(build_uuid, ml_platform, options, start, stop, Nil)
+          })
+
+      for (build <- builds.sortBy(_.start)(Date.Ordering)) yield {
+        val sessions = Data.read_sessions_domain(db, build_uuid = build.build_uuid)
+        build.copy(sessions = sessions.toList.sorted)
+      }
+    }
 
     def start_build(
       db: SQL.Database,
@@ -793,11 +801,6 @@
 
   def read_builds(db: SQL.Database): List[Build] =
     Data.transaction_lock(db, create = true) { Data.read_builds(db) }
-
-  def read_sessions(db: SQL.Database, build_uuid: String = ""): List[String] =
-    Data.transaction_lock(db, create = true) {
-      Data.read_sessions_domain(db, build_uuid = build_uuid).toList.sorted
-    }
 }