--- 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"
--- 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)
--- 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)))
--- 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)
--- 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 =
--- 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)