diff -r d7eb6a4522b8 -r 57fdb6c846b0 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,