tuned messages: avoid duplicates;

--- a/src/Pure/Tools/build_process.scala	Sun Aug 27 12:57:59 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Aug 27 13:15:32 2023 +0200
@@ -1101,6 +1101,11 @@
     def sleep(): Unit =
       Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
 
+    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(): Boolean = synchronized_database("Build_Process.check_jobs") {
       val jobs = next_jobs(_state)
       for (name <- jobs) {
@@ -1109,13 +1114,12 @@
             _state.ancestor_results(name) match {
               case Some(results) => _state = start_session(_state, name, results)
               case None =>
-                build_progress.echo_warning(
-                  "Broken build job " + quote(name) + ": no ancestor results")
+                build_progress_warning("Bad build job " + quote(name) + ": no ancestor results")
             }
           }
-          else build_progress.echo_warning("Broken build job " + quote(name) + ": no session info")
+          else build_progress_warning("Bad build job " + quote(name) + ": no session info")
         }
-        else build_progress.echo_warning("Unsupported build job " + quote(name))
+        else build_progress_warning("Bad build job " + quote(name))
       }
       jobs.nonEmpty
     }