clarified signature: prefer static percentage;

--- a/src/Pure/PIDE/document_status.scala	Wed Sep 24 21:52:03 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 24 22:18:52 2025 +0200
@@ -261,6 +261,13 @@
         if (t.is_notable(threshold)) command_timings += (command -> status.timings)
       }
 
+      val total = unprocessed + running + warned + failed + finished
+
+      val percentage: Int =
+        if (Theory_Status.consolidated(theory_status)) 100
+        else if (total == 0) 0
+        else (((total - unprocessed).toDouble / total) * 100).toInt min 99
+
       Node_Status(
         theory_status = theory_status,
         suppressed = version.nodes.suppressed(name),
@@ -274,7 +281,8 @@
         total_timing = total_timing,
         max_time = max_time,
         threshold = threshold,
-        command_timings = command_timings)
+        command_timings = command_timings,
+        percentage)
     }
   }
 
@@ -291,7 +299,8 @@
     total_timing: Timing = Timing.zero,
     max_time: Time = Time.zero,
     threshold: Time = Time.zero,
-    command_timings: Map[Command, Command_Timings] = Map.empty
+    command_timings: Map[Command, Command_Timings] = Map.empty,
+    percentage: Int = 0
   ) extends Theory_Status {
     def is_empty: Boolean = this == Node_Status.empty
 
@@ -300,11 +309,6 @@
 
     def quasi_consolidated: Boolean = !suppressed && !finalized && terminated
 
-    def percentage: Int =
-      if (consolidated) 100
-      else if (total == 0) 0
-      else (((total - unprocessed).toDouble / total) * 100).toInt min 99
-
     def json: JSON.Object.T =
       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,