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