--- a/src/Pure/PIDE/document_status.scala Tue Nov 04 21:49:24 2025 +0100
+++ b/src/Pure/PIDE/document_status.scala Tue Nov 04 22:09:26 2025 +0100
@@ -56,6 +56,8 @@
def is_empty: Boolean = running.isEmpty && finished.isEmpty
def has_running: Boolean = running.nonEmpty
+ def long_running(now: Date, threshold: Time): List[Command_Running] =
+ List.from(for (run <- running.valuesIterator if run.time(now) >= threshold) yield run)
def add_running(entry: Command_Timings.Entry_Running): Command_Timings =
new Command_Timings(running + entry, finished, sum_finished)