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