diff -r e8db2209d21d -r 03dfb684a50d src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun Oct 19 13:45:07 2025 +0200
+++ b/src/Pure/System/progress.scala	Sun Oct 19 14:05:58 2025 +0200
@@ -68,6 +68,11 @@
       if (cumulated_time.is_relevant) " (" + cumulated_time.message + " cumulated time)" else ""
   }
 
+  object Nodes_Status {
+    def empty(session: String): Nodes_Status =
+      Nodes_Status(Nil, Document_Status.Nodes_Status.empty, session = session)
+  }
+
   sealed case class Nodes_Status(
     domain: List[Document.Node.Name],
     document_status: Document_Status.Nodes_Status,