diff -r dc96e6c56369 -r afb1a19307c4 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Mon Mar 13 20:24:13 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Mon Mar 13 21:12:34 2023 +0100 @@ -459,7 +459,16 @@ }) } - def sync_progress(db: SQL.Database, build_uuid: String, build_progress: Progress): Unit = { + def sync_progress( + db: SQL.Database, + seen: Long, + build_uuid: String, + build_progress: Progress + ): (Progress_Messages, Boolean) = { + require(build_uuid.nonEmpty) + + val messages = read_progress(db, seen = seen, build_uuid = build_uuid) + val stopped_db = db.execute_query_statementO[Boolean]( Base.table.select(List(Base.progress_stopped), @@ -477,6 +486,8 @@ if (stopped_db && !stopped) build_progress.stop() if (stopped && !stopped_db) stop_db() + + (messages, messages.isEmpty && stopped_db == stopped) } @@ -823,10 +834,25 @@ _database match { case None => body case Some(db) => - db.transaction_lock(Build_Process.Data.all_tables) { - Build_Process.Data.sync_progress(db, build_uuid, build_progress) - body + @tailrec def loop(): A = { + val sync_progress = + db.transaction_lock(Build_Process.Data.all_tables) { + val (messages, sync) = + Build_Process.Data.sync_progress( + db, _state.progress_seen, build_uuid, build_progress) + if (sync) Left(body) else Right(messages) + } + sync_progress match { + case Left(res) => res + case Right(messages) => + for ((message_serial, message) <- messages) { + _state = _state.progress_serial(message_serial = message_serial) + if (build_progress.do_output(message)) build_progress.output(message) + } + loop() + } } + loop() } }