# HG changeset patch
# User wenzelm
# Date 1692295584 -7200
# Node ID 555bdac7c279a8f36505df0d625a4edda84b632b
# Parent  af37e1b4dce0c4db9881ad3b1c78f0d3ca0c8bf2
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;

diff -r af37e1b4dce0 -r 555bdac7c279 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu Aug 17 19:01:40 2023 +0200
+++ b/src/Pure/System/progress.scala	Thu Aug 17 20:06:24 2023 +0200
@@ -265,6 +265,7 @@
 class Database_Progress(
   db: SQL.Database,
   base_progress: Progress,
+  input_messages: Boolean = false,
   output_stopped: Boolean = false,
   kind: String = "progress",
   hostname: String = Isabelle_System.hostname(),
@@ -370,12 +371,19 @@
         Progress.private_data.write_progress_stopped(db, _context, true)
       }
 
-      val messages = Progress.private_data.read_messages(db, _context, seen = _serial)
-      for ((message_serial, message) <- messages) {
-        if (base_progress.do_output(message)) base_progress.output(message)
-        _serial = _serial max message_serial
+      val serial0 = _serial
+      if (input_messages) {
+        val messages = Progress.private_data.read_messages(db, _context, seen = _serial)
+        for ((message_serial, message) <- messages) {
+          if (base_progress.do_output(message)) base_progress.output(message)
+          _serial = _serial max message_serial
+        }
       }
-      if (messages.nonEmpty) Progress.private_data.update_agent(db, _agent_uuid, _serial)
+      else {
+        _serial = _serial max Progress.private_data.read_messages_serial(db, _context)
+      }
+
+      if (_serial != serial0) Progress.private_data.update_agent(db, _agent_uuid, _serial)
 
       body
     }
diff -r af37e1b4dce0 -r 555bdac7c279 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Aug 17 19:01:40 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Aug 17 20:06:24 2023 +0200
@@ -882,6 +882,7 @@
           val progress_db = store.open_build_database(Progress.private_data.database, server = server)
           val progress =
             new Database_Progress(progress_db, build_progress,
+              input_messages = build_context.master,
               output_stopped = build_context.master,
               hostname = hostname,
               context_uuid = build_uuid,