src/Pure/PIDE/document_status.scala
changeset 83507 989304e45ad7
parent 83505 ef6863b14ca2
--- 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)