more robust "stop": further "stamp" ticks may happen afterwards;

--- a/src/Pure/System/progress.scala	Sun Jul 02 19:51:03 2023 +0200
+++ b/src/Pure/System/progress.scala	Sun Jul 02 20:09:12 2023 +0200
@@ -107,17 +107,22 @@
       db: SQL.Database,
       agent_uuid: String,
       seen: Long,
-      stop: Boolean = false
+      stop_now: Boolean = false
     ): Unit = {
-      val sql =
-        Agents.table.update(List(Agents.stamp, Agents.stop, Agents.seen),
-          sql = Agents.agent_uuid.where_equal(agent_uuid))
-      db.execute_statement(sql, body = { stmt =>
-        val now = db.now()
-        stmt.date(1) = now
-        stmt.date(2) = if (stop) Some(now) else None
-        stmt.long(3) = seen
-      })
+      val sql = Agents.agent_uuid.where_equal(agent_uuid)
+
+      val stop =
+        db.execute_query_statementO(
+          Agents.table.select(List(Agents.stop), sql = sql), _.get_date(Agents.stop)).flatten
+
+      db.execute_statement(
+        Agents.table.update(List(Agents.stamp, Agents.stop, Agents.seen), sql = sql),
+        body = { stmt =>
+          val now = db.now()
+          stmt.date(1) = now
+          stmt.date(2) = if (stop_now) Some(now) else stop
+          stmt.long(3) = seen
+        })
     }
 
     def next_messages_serial(db: SQL.Database, context: Long): Long =
@@ -290,7 +295,7 @@
   def exit(close: Boolean = false): Unit = synchronized {
     if (_context > 0) {
       Progress.Data.transaction_lock(db) {
-        Progress.Data.update_agent(db, _agent_uuid, _seen, stop = true)
+        Progress.Data.update_agent(db, _agent_uuid, _seen, stop_now = true)
       }
       _context = 0
     }

--- a/src/Pure/Tools/build_process.scala	Sun Jul 02 19:51:03 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 02 20:09:12 2023 +0200
@@ -548,15 +548,20 @@
       db: SQL.Database,
       worker_uuid: String,
       serial: Long,
-      stop: Boolean = false
+      stop_now: Boolean = false
     ): Unit = {
+      val sql = Workers.worker_uuid.where_equal(worker_uuid)
+
+      val stop =
+        db.execute_query_statementO(
+          Workers.table.select(List(Workers.stop), sql = sql), _.get_date(Workers.stop)).flatten
+
       db.execute_statement(
-        Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial),
-          sql = Workers.worker_uuid.where_equal(worker_uuid)),
+        Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial), sql = sql),
         body = { stmt =>
           val now = db.now()
           stmt.date(1) = now
-          stmt.date(2) = if (stop) Some(now) else None
+          stmt.date(2) = if (stop_now) Some(now) else stop
           stmt.long(3) = serial
         })
     }
@@ -1038,7 +1043,7 @@
 
   protected final def stop_worker(): Unit = synchronized_database {
     for (db <- _build_database) {
-      Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop = true)
+      Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop_now = true)
     }
   }