--- a/src/Pure/System/progress.scala Thu Aug 10 16:49:17 2023 +0200
+++ b/src/Pure/System/progress.scala Thu Aug 10 16:57:01 2023 +0200
@@ -348,9 +348,9 @@
private def output_database(out: Progress.Output): Unit =
sync_database {
- val serial = Progress.private_data.next_messages_serial(db, _context)
+ _serial = _serial max Progress.private_data.next_messages_serial(db, _context)
- Progress.private_data.write_messages(db, _context, serial, out.message)
+ Progress.private_data.write_messages(db, _context, _serial, out.message)
out match {
case message: Progress.Message =>
@@ -358,7 +358,6 @@
case theory: Progress.Theory => base_progress.theory(theory)
}
- _serial = _serial max serial
Progress.private_data.update_agent(db, _agent_uuid, _serial)
}