diff -r 2cb50474958a -r a3c59c842625 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Mon Oct 13 23:01:15 2025 +0200 +++ b/src/Pure/System/progress.scala Wed Oct 15 11:11:33 2025 +0200 @@ -100,7 +100,7 @@ /* status lines (e.g. at bottom of output) */ trait Status extends Progress { - def status_enabled: Boolean = false + def status_detailed: Boolean = false def status_hide(status: Progress.Output): Unit = () protected var _status: Progress.Output = Nil @@ -129,7 +129,7 @@ override def nodes_status(nodes_status: Progress.Nodes_Status): Unit = synchronized { status_clear() output(nodes_status.completed_theories) - status_output(if (status_enabled) nodes_status.status_theories else Nil) + status_output(if (status_detailed) nodes_status.status_theories else Nil) } } } @@ -208,7 +208,7 @@ detailed: Boolean = false, stderr: Boolean = false) extends Progress with Progress.Status { - override def status_enabled: Boolean = detailed + 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)