--- a/src/Pure/Build/build.scala Sat Oct 11 16:19:16 2025 +0200
+++ b/src/Pure/Build/build.scala Sun Oct 12 15:11:29 2025 +0200
@@ -22,17 +22,6 @@
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 */
sealed case class Context(
@@ -180,6 +169,8 @@
/* build */
+ def progress_detailed(options: Options): Boolean = options.bool("build_progress")
+
def build(
options: Options,
private_dir: Option[Path] = None,
@@ -441,7 +432,8 @@
val sessions = getopts(args)
- val progress = new Build_Progress(options, verbose = verbose)
+ val progress =
+ new Console_Progress(verbose = verbose, detailed = progress_detailed(options))
val ml_settings = ML_Settings(options)