src/Pure/Build/build.scala
changeset 83223 a225609e3344
parent 82996 4a77ce6d4e07
child 83226 37b61794a93a
--- a/src/Pure/Build/build.scala	Tue Sep 23 12:36:36 2025 +0200
+++ b/src/Pure/Build/build.scala	Tue Sep 23 13:11:52 2025 +0200
@@ -22,6 +22,16 @@
   def engine_name(options: Options): String = options.string("build_engine")
 
 
+  /* detailed build progress */
+
+  class Build_Progress(options: Options, verbose: Boolean = false)
+  extends Console_Progress(verbose = verbose) {
+    override def nodes_status(nodes_status: Progress.Nodes_Status): Unit =
+      if (options.bool("build_progress")) {
+        output(nodes_status.message.copy(verbose = false))
+      }
+  }
+
 
   /* context */
 
@@ -431,7 +441,7 @@
 
       val sessions = getopts(args)
 
-      val progress = new Console_Progress(verbose = verbose)
+      val progress = new Build_Progress(options, verbose = verbose)
 
       val ml_settings = ML_Settings(options)