# HG changeset patch
# User wenzelm
# Date 1709556911 -3600
# Node ID 5857bb16cf30eed3e5aeab1f8ee15043ea8faab8
# Parent  8fa5b82a6964249c401757467a4cddd3181baf3c
clarified module signature and state;

diff -r 8fa5b82a6964 -r 5857bb16cf30 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Mon Mar 04 13:44:11 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Mon Mar 04 13:55:11 2024 +0100
@@ -850,6 +850,14 @@
   protected final val hostname: String = build_context.hostname
   protected final val build_uuid: String = build_context.build_uuid
 
+  private var warning_seen = Set.empty[String]
+  protected def warning(msg: String): Unit = synchronized {
+    if (!warning_seen(msg)) {
+      build_progress.echo_warning(msg)
+      warning_seen += msg
+    }
+  }
+
 
   /* global resources with common close() operation */
 
@@ -1137,11 +1145,6 @@
       finished = finished_unsynchronized()
     }
 
-    val build_progress_warnings = Synchronized(Set.empty[String])
-    def build_progress_warning(msg: String): Unit =
-      build_progress_warnings.change(seen =>
-        if (seen(msg)) seen else { build_progress.echo_warning(msg); seen + msg })
-
     def check_jobs_unsynchronized(): Boolean = {
       val jobs = next_jobs(_state)
       for (name <- jobs) {
@@ -1149,13 +1152,12 @@
           if (build_context.sessions_structure.defined(name)) {
             _state.ancestor_results(name) match {
               case Some(results) => _state = start_session(_state, name, results)
-              case None =>
-                build_progress_warning("Bad build job " + quote(name) + ": no ancestor results")
+              case None => warning("Bad build job " + quote(name) + ": no ancestor results")
             }
           }
-          else build_progress_warning("Bad build job " + quote(name) + ": no session info")
+          else warning("Bad build job " + quote(name) + ": no session info")
         }
-        else build_progress_warning("Bad build job " + quote(name))
+        else warning("Bad build job " + quote(name))
       }
       jobs.nonEmpty
     }