--- a/src/Pure/Build/database_progress.scala Mon Oct 13 14:24:27 2025 +0200
+++ b/src/Pure/Build/database_progress.scala Mon Oct 13 14:44:46 2025 +0200
@@ -156,7 +156,7 @@
context_uuid: String = UUID.random_string(),
timeout: Option[Time] = None,
tick_expire: Int = 50)
-extends Progress {
+extends Progress with Progress.Status {
database_progress =>
override def now(): Date = db.now()
@@ -311,9 +311,6 @@
override def output(message: Progress.Message): Unit = sync_context { _consumer.send(message) }
override def theory(theory: Progress.Theory): Unit = sync_context { _consumer.send(theory) }
- override def nodes_status(nodes_status: Progress.Nodes_Status): Unit =
- base_progress.nodes_status(nodes_status)
-
override def verbose: Boolean = base_progress.verbose
override def stop(): Unit = sync_context { base_progress.stop(); sync() }