# HG changeset patch
# User wenzelm
# Date 1758743523 -7200
# Node ID 2ecfd436903b0e779ff4cae8fd40cba4b7c68fe8
# Parent  37b61794a93aa5840b6e48a1dcc1a9b331a7d617
more informative Progress.Nodes_Status;

diff -r 37b61794a93a -r 2ecfd436903b src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Wed Sep 24 17:41:36 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Wed Sep 24 21:52:03 2025 +0200
@@ -239,7 +239,8 @@
                 val result =
                   if (nodes_changed.isEmpty) None
                   else {
-                    Some(Progress.Nodes_Status(nodes_domain, nodes_status1, session = session_name))
+                    Some(Progress.Nodes_Status(
+                      nodes_domain, nodes_status1, session = session_name, old = Some(nodes_status)))
                   }
 
                 nodes_changed = Set.empty
diff -r 37b61794a93a -r 2ecfd436903b src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Wed Sep 24 17:41:36 2025 +0200
+++ b/src/Pure/System/progress.scala	Wed Sep 24 21:52:03 2025 +0200
@@ -54,7 +54,8 @@
   sealed case class Nodes_Status(
     domain: List[Document.Node.Name],
     document_status: Document_Status.Nodes_Status,
-    session: String = ""
+    session: String = "",
+    old: Option[Document_Status.Nodes_Status] = None
   ) {
     def message: Message =
       Message(Kind.writeln, cat_lines(domain.map(name => theory(name).message.text)),