src/Pure/System/progress.scala
changeset 83280 a3c59c842625
parent 83271 93db1865ee0e
child 83282 4643bb10d188
--- 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)