build_progress with percentage;

--- a/src/Pure/PIDE/document.scala	Wed Sep 24 22:18:52 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Sep 24 22:47:04 2025 +0200
@@ -323,6 +323,10 @@
     def load_commands_changed(doc_blobs: Blobs): Boolean =
       load_commands.exists(_.blobs_changed(doc_blobs))
 
+    def get_theory: Option[Command] =
+      if (commands.size == 1 && commands.last.span.is_theory) Some(commands.last)
+      else None
+
     def update_header(new_header: Node.Header): Node =
       new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 

--- a/src/Pure/PIDE/document_status.scala	Wed Sep 24 22:18:52 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 24 22:47:04 2025 +0200
@@ -229,6 +229,8 @@
       name: Document.Node.Name,
       threshold: Time = Time.max
     ): Node_Status = {
+      val node = version.nodes(name)
+
       var theory_status = Document_Status.Theory_Status.NONE
       var unprocessed = 0
       var running = 0
@@ -241,7 +243,7 @@
       var max_time = Time.zero
       var command_timings = Map.empty[Command, Command_Timings]
 
-      for (command <- version.nodes(name).commands.iterator) {
+      for (command <- node.commands.iterator) {
         val status = state.command_status(version, command)
 
         theory_status = Theory_Status.merge(theory_status, status.theory_status)
@@ -261,12 +263,23 @@
         if (t.is_notable(threshold)) command_timings += (command -> status.timings)
       }
 
-      val total = unprocessed + running + warned + failed + finished
+      def percent(a: Int, b: Int): Int =
+        if (b == 0) 0 else ((a.toDouble / b) * 100).toInt
 
-      val percentage: Int =
-        if (Theory_Status.consolidated(theory_status)) 100
-        else if (total == 0) 0
-        else (((total - unprocessed).toDouble / total) * 100).toInt min 99
+      val percentage: Int = {
+        node.get_theory match {
+          case None =>
+            if (Theory_Status.consolidated(theory_status)) 100
+            else {
+              val total = unprocessed + running + warned + failed + finished
+              percent(total - unprocessed, total).min(99)
+            }
+          case Some(command) =>
+            val total = command.span.theory_commands
+            val processed = state.command_status(version, command).timings.count
+            percent(processed, total)
+        }
+      }
 
       Node_Status(
         theory_status = theory_status,

--- a/src/Pure/System/progress.scala	Wed Sep 24 22:18:52 2025 +0200
+++ b/src/Pure/System/progress.scala	Wed Sep 24 22:47:04 2025 +0200
@@ -66,7 +66,9 @@
 
     def theory(name: Document.Node.Name): Theory = {
       val node_status = apply(name)
-      Theory(theory = name.theory, session = session, total_time = node_status.total_timing.elapsed)
+      Theory(theory = name.theory, session = session,
+        percentage = Some(node_status.percentage),
+        total_time = node_status.total_timing.elapsed)
     }
   }
 }