basic setup for build progress with nodes_status;

--- a/etc/options	Sun Sep 21 19:47:26 2025 +0200
+++ b/etc/options	Sun Sep 21 23:48:59 2025 +0200
@@ -212,6 +212,9 @@
 option build_database_slice : real = 300 for build_sync
   -- "slice size in MiB for ML heap stored within database"
 
+option build_progress_delay : real = 2
+  -- "delay for detailed build progress"
+
 option build_delay : real = 0.2
   -- "delay for build process main loop (local)"
 

--- a/src/Pure/Build/build_job.scala	Sun Sep 21 19:47:26 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Sun Sep 21 23:48:59 2025 +0200
@@ -121,7 +121,9 @@
         val options = Host.node_options(info.options, node_info)
         val store = build_context.store
 
+        val build_progress_delay: Time = options.seconds("build_progress_delay")
         val build_timing_threshold: Time = options.seconds("build_timing_threshold")
+        val editor_timing_threshold: Time = options.seconds("editor_timing_threshold")
 
         using_optional(store.maybe_open_database_server(server = server)) { database_server =>
           store.clean_output(database_server, session_name, session_init = true)
@@ -216,6 +218,34 @@
           val session_timings = new mutable.ListBuffer[Properties.T]
           val runtime_statistics = new mutable.ListBuffer[Properties.T]
           val task_statistics = new mutable.ListBuffer[Properties.T]
+          var nodes_changed = Set.empty[Document_ID.Generic]
+          var nodes_status = Document_Status.Nodes_Status.empty
+
+          val nodes_domain = build_context.deps(session_name).used_theories.map(_._1)
+
+          def nodes_status_progress(): Unit = {
+            val state = session.get_state()
+            val result =
+              session.synchronized {
+                val nodes_status1 =
+                  nodes_changed.foldLeft(nodes_status)( { case (status, state_id) =>
+                    state.theory_snapshot(state_id, session.build_blobs) match {
+                      case None => status
+                      case Some(snapshot) =>
+                        status.update_node(snapshot.state, snapshot.version, snapshot.node_name,
+                          threshold = editor_timing_threshold)
+                    }
+                  }
+                )
+                val updated = nodes_status1 != nodes_status
+                nodes_changed = Set.empty
+                nodes_status = nodes_status1
+                if (updated) Some (nodes_status1) else None
+              }
+            result.foreach(progress.nodes_status(nodes_domain, _))
+          }
+
+          val nodes_delay = Delay.first(build_progress_delay) { nodes_status_progress() }
 
           def fun(
             name: String,
@@ -279,14 +309,15 @@
             })
 
           session.command_timings += Session.Consumer("command_timings") {
-            case Session.Command_Timing(props) =>
-              for {
-                elapsed <- Markup.Elapsed.unapply(props)
-                if Time.seconds(elapsed).is_notable(build_timing_threshold)
-              } {
-                session.synchronized {
-                  command_timings += props.filter(Markup.command_timing_property)
-                }
+            case Session.Command_Timing(state_id, props) =>
+              session.synchronized {
+                for {
+                  elapsed <- Markup.Elapsed.unapply(props)
+                  if Time.seconds(elapsed).is_notable(build_timing_threshold)
+                } command_timings += props.filter(Markup.command_timing_property)
+
+                nodes_changed += state_id
+                nodes_delay.invoke()
               }
           }
 
@@ -398,6 +429,9 @@
 
           session.stop()
 
+          nodes_delay.revoke()
+          nodes_status_progress()
+
           val export_errors =
             export_consumer.shutdown(close = true).map(Output.error_message_text)
 

--- a/src/Pure/PIDE/document.scala	Sun Sep 21 19:47:26 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Sep 21 23:48:59 2025 +0200
@@ -1106,6 +1106,9 @@
           (state1.snippet(List(command1), doc_blobs), state1)
       }
 
+    def theory_snapshot(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): Option[Snapshot] =
+      if (theories.isDefinedAt(id)) Some(end_theory(id, document_blobs)._1) else None
+
     def assign(
       id: Document_ID.Version,
       edited: List[String],

--- a/src/Pure/PIDE/session.scala	Sun Sep 21 19:47:26 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sun Sep 21 23:48:59 2025 +0200
@@ -63,7 +63,7 @@
   /* events */
 
   //{{{
-  case class Command_Timing(props: Properties.T)
+  case class Command_Timing(state_id: Document_ID.Generic, props: Properties.T)
   case class Theory_Timing(props: Properties.T)
   case class Runtime_Statistics(props: Properties.T)
   case class Task_Statistics(props: Properties.T)
@@ -538,7 +538,7 @@
               case Protocol.Command_Timing(state_id, props) if prover.defined =>
                 val message = XML.elem(Markup.STATUS, List(XML.elem(Markup(Markup.TIMING, props))))
                 change_command(_.accumulate(state_id, cache.elem(message), cache))
-                command_timings.post(Session.Command_Timing(props))
+                command_timings.post(Session.Command_Timing(state_id, props))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))