diff -r 4729ac19c03c -r 8767da4c15a8 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Tue Nov 04 22:38:09 2025 +0100 +++ b/src/Pure/System/progress.scala Wed Nov 05 12:16:17 2025 +0100 @@ -112,7 +112,7 @@ else None }) - def status_commands(threshold: Time): List[Progress.Message] = + def long_running_commands(threshold: Time, status: Boolean = false): List[Progress.Message] = List.from( for { name <- domain.iterator @@ -124,7 +124,7 @@ if_proper(session, session + ": ") + "command " + quote(run.name) + " running for " + run.time(now).message + " (line " + run.line + " of theory " + quote(name.theory) + ")" - Progress.Message(Progress.Kind.writeln, text, verbose = true) + Progress.Message(Progress.Kind.writeln, text, verbose = true, status = status) }) } @@ -163,6 +163,10 @@ } override def nodes_status(nodes_status: Progress.Nodes_Status): Unit = synchronized { + val long_running_commands = + nodes_status.long_running_commands(status_threshold, status = status_detailed) + val output_commands = if (status_detailed) Nil else long_running_commands + val old_status = status_clear() val new_status = { val buf = new mutable.ListBuffer[(String, Progress.Msg)] @@ -170,12 +174,13 @@ for (old <- old_status if old._1 < session) buf += old if (status_detailed) { for (thy <- nodes_status.status_theories) buf += (session -> thy) + for (msg <- long_running_commands) buf += (session -> msg) } for (old <- old_status if old._1 > session) buf += old buf.toList } - output(nodes_status.completed_theories ::: nodes_status.status_commands(status_threshold)) + output(nodes_status.completed_theories ::: output_commands) output_status(new_status) } }