# HG changeset patch
# User wenzelm
# Date 1762290566 -3600
# Node ID 989304e45ad785aece8e61233183b02a5d21604f
# Parent  b1e04ffb4b086a6b2379f9fcc84cdd56822288c0
progress for long-running commands;

diff -r b1e04ffb4b08 -r 989304e45ad7 etc/options
--- a/etc/options	Tue Nov 04 21:49:24 2025 +0100
+++ b/etc/options	Tue Nov 04 22:09:26 2025 +0100
@@ -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_threshold : real = 20 for build
+  -- "threshold for long-running commands (seconds)"
+
 option build_progress_detailed : bool = false for build
   -- "detailed status for ongoing build progress"
 
diff -r b1e04ffb4b08 -r 989304e45ad7 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Tue Nov 04 21:49:24 2025 +0100
+++ b/src/Pure/Build/build.scala	Tue Nov 04 22:09:26 2025 +0100
@@ -169,6 +169,7 @@
 
   /* build */
 
+  def progress_threshold(options: Options): Time = options.seconds("build_progress_threshold")
   def progress_detailed(options: Options): Boolean = options.bool("build_progress_detailed")
 
   def build(
@@ -433,7 +434,9 @@
       val sessions = getopts(args)
 
       val progress =
-        new Console_Progress(verbose = verbose, detailed = progress_detailed(options))
+        new Console_Progress(verbose = verbose,
+          threshold = progress_threshold(options),
+          detailed = progress_detailed(options))
 
       val ml_settings = ML_Settings(options)
 
diff -r b1e04ffb4b08 -r 989304e45ad7 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Tue Nov 04 21:49:24 2025 +0100
+++ b/src/Pure/Build/build_job.scala	Tue Nov 04 22:09:26 2025 +0100
@@ -160,6 +160,7 @@
     private def nodes_status_progress(state: Document.State = get_state()): Unit = {
       val result =
         synchronized {
+          lazy val now = progress.now()
           for (id <- state.progress_theories if !nodes_changed(id)) nodes_changed += id
           val nodes_status1 =
             nodes_changed.foldLeft(nodes_status)({ case (status, state_id) =>
@@ -167,7 +168,7 @@
                 case None => status
                 case Some(snapshot) =>
                   Exn.Interrupt.expose()
-                  status.update_node(progress.now(),
+                  status.update_node(now,
                     snapshot.state, snapshot.version, snapshot.node_name,
                     threshold = editor_timing_threshold)
               }
@@ -175,7 +176,7 @@
           val result =
             if (nodes_changed.isEmpty) None
             else {
-              Some(Progress.Nodes_Status(
+              Some(Progress.Nodes_Status(now,
                 nodes_domain, nodes_status1,
                 session = resources.session_background.session_name,
                 old = Some(nodes_status)))
diff -r b1e04ffb4b08 -r 989304e45ad7 src/Pure/PIDE/document_status.scala
--- 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)
 
diff -r b1e04ffb4b08 -r 989304e45ad7 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Nov 04 21:49:24 2025 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Nov 04 22:09:26 2025 +0100
@@ -354,8 +354,9 @@
         val delay_nodes_status =
           Delay.first(nodes_status_delay max Time.zero) {
             val st = use_theories_state.value
+            val now = progress.now()
             progress.nodes_status(
-              Progress.Nodes_Status(st.dep_graph.topological_order, st.nodes_status))
+              Progress.Nodes_Status(now, st.dep_graph.topological_order, st.nodes_status))
           }
 
         val delay_commit_clean =
diff -r b1e04ffb4b08 -r 989304e45ad7 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Nov 04 21:49:24 2025 +0100
+++ b/src/Pure/System/progress.scala	Tue Nov 04 22:09:26 2025 +0100
@@ -70,10 +70,11 @@
 
   object Nodes_Status {
     def empty(session: String): Nodes_Status =
-      Nodes_Status(Nil, Document_Status.Nodes_Status.empty, session = session)
+      Nodes_Status(Date.now(), Nil, Document_Status.Nodes_Status.empty, session = session)
   }
 
   sealed case class Nodes_Status(
+    now: Date,
     domain: List[Document.Node.Name],
     document_status: Document_Status.Nodes_Status,
     session: String = "",
@@ -110,15 +111,33 @@
         }
         else None
       })
+
+    def status_commands(threshold: Time): List[Progress.Message] =
+      List.from(
+        for {
+          name <- domain.iterator
+          st = apply(name)
+          command_timings <- st.command_timings.valuesIterator
+          run <- command_timings.long_running(now, threshold).iterator
+        } yield {
+          val text =
+            if_proper(session, session + ": ") +
+              "long-running command " + quote(run.name) +
+              " (" + run.time(now).message + " at line " + run.line +
+              " of theory " + quote(name.theory) + ")"
+          Progress.Message(Progress.Kind.writeln, text, verbose = true, status = true)
+        })
   }
 
 
   /* status lines (e.g. at bottom of output) */
 
   trait Status extends Progress {
+    def status_threshold: Time = Time.zero
+    def status_detailed: Boolean = false
+
     def status_output(msgs: Progress.Output): Unit
 
-    def status_detailed: Boolean = false
     def status_hide(status: Progress.Output): Unit = ()
 
     protected var _status: Progress.Session_Output = Nil
@@ -150,7 +169,12 @@
         val buf = new mutable.ListBuffer[(String, Progress.Msg)]
         val session = nodes_status.session
         for (old <- old_status if old._1 < session) buf += old
-        if (status_detailed) { for (thy <- nodes_status.status_theories) buf += (session -> thy) }
+        if (status_detailed) {
+          for (thy <- nodes_status.status_theories) buf += (session -> thy)
+          for (msg <- nodes_status.status_commands(status_threshold)) {
+            buf += (session -> msg)
+          }
+        }
         for (old <- old_status if old._1 > session) buf += old
         buf.toList
       }
@@ -232,10 +256,13 @@
 
 class Console_Progress(
   override val verbose: Boolean = false,
+  threshold: Time = Time.zero,
   detailed: Boolean = false,
   stderr: Boolean = false)
 extends Progress with Progress.Status {
+  override def status_threshold: Time = threshold
   override def status_detailed: Boolean = detailed
+
   override def status_hide(status: Progress.Output): Unit = synchronized {
     val txt = output_text(status, terminate = true)
     Output.delete_lines(Library.count_newlines(txt), stdout = !stderr)