diff -r 92ef737f412c -r cf114894a5ed src/Pure/Tools/build_process.scala --- 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 }