--- 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
}