# HG changeset patch
# User wenzelm
# Date 1677968730 -3600
# Node ID f5d6cd98b16aaabb24ba0c60d01b79f14d440d1e
# Parent  3bc49507bae55b2c714a286cea116b3161d02786
clarified signature: manage "verbose" flag via "progress";

diff -r 3bc49507bae5 -r f5d6cd98b16a src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -43,7 +43,6 @@
     select_dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
-    verbose: Boolean = false
   ): Build.Results = {
     require(!selection.requirements)
     Isabelle_System.make_directory(output_dir)
@@ -53,7 +52,7 @@
       Build.build(options, build_heap = true,
         selection = selection.copy(requirements = true), progress = progress, dirs = dirs,
         select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
-        verbose = verbose)
+        verbose = progress.verbose)
 
     if (build_results0.ok) {
       val build_options =
@@ -71,10 +70,9 @@
             case msg: Prover.Protocol_Output =>
               msg.properties match {
                 case Protocol.Export(args) if args.name.startsWith("mirabelle/") =>
-                  if (verbose) {
-                    progress.echo(
-                      "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")")
-                  }
+                  progress.echo(
+                    "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")",
+                    verbose = true)
                   val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = build_results0.cache)
                   val lines = Pretty.string_of(yxml).trim()
                   val prefix =
@@ -97,7 +95,7 @@
 
       Build.build(build_options, clean_build = true,
         selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs,
-        numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose,
+        numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = progress.verbose,
         session_setup = session_setup)
     }
     else build_results0
@@ -197,9 +195,7 @@
 
       val start_date = Date.now()
 
-      if (verbose) {
-        progress.echo("Started at " + Build_Log.print_date(start_date))
-      }
+      progress.echo("Started at " + Build_Log.print_date(start_date), verbose = true)
 
       val results =
         progress.interrupt_handler {
@@ -216,16 +212,13 @@
             dirs = dirs,
             select_dirs = select_dirs,
             numa_shuffling = Host.numa_check(progress, numa_shuffling),
-            max_jobs = max_jobs,
-            verbose = verbose)
+            max_jobs = max_jobs)
         }
 
       val end_date = Date.now()
       val elapsed_time = end_date.time - start_date.time
 
-      if (verbose) {
-        progress.echo("\nFinished at " + Build_Log.print_date(end_date))
-      }
+      progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
 
       val total_timing =
         results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -49,7 +49,6 @@
 
   def build_csdp(
     download_url: String = default_download_url,
-    verbose: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current,
     mingw: MinGW = MinGW.none
@@ -112,7 +111,9 @@
             foreach(file => flags.change(File.path(file)))
       }
 
-      progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check
+      progress.bash(mingw.bash_script("make"),
+        cwd = source_dir.file,
+        echo = progress.verbose).check
 
 
       /* install */
@@ -188,9 +189,9 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
-        build_csdp(download_url = download_url, verbose = verbose, progress = progress,
+        build_csdp(download_url = download_url, progress = progress,
           target_dir = target_dir, mingw = mingw)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_e.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -16,7 +16,6 @@
   def build_e(
     version: String = default_version,
     download_url: String = default_download_url,
-    verbose: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
@@ -58,8 +57,8 @@
 
       val build_script = "./configure" + build_options + " && make"
       Isabelle_System.bash(build_script, cwd = source_dir.file,
-        progress_stdout = progress.echo_if(verbose, _),
-        progress_stderr = progress.echo_if(verbose, _)).check
+        progress_stdout = progress.echo(_, verbose = true),
+        progress_stderr = progress.echo(_, verbose = true)).check
 
 
       /* install */
@@ -131,9 +130,9 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
         build_e(version = version, download_url = download_url,
-          verbose = verbose, progress = progress, target_dir = target_dir)
+          progress = progress, target_dir = target_dir)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_minisat.scala
--- a/src/Pure/Admin/build_minisat.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_minisat.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -18,7 +18,6 @@
   def build_minisat(
     download_url: String = default_download_url,
     component_name: String = "",
-    verbose: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
@@ -77,7 +76,7 @@
           _.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
         }
       }
-      progress.bash("make r", source_dir.file, echo = verbose).check
+      progress.bash("make r", source_dir.file, echo = progress.verbose).check
 
       Isabelle_System.copy_file(
         source_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
@@ -142,9 +141,9 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
         build_minisat(download_url = download_url, component_name = component_name,
-          verbose = verbose, progress = progress, target_dir = target_dir)
+          progress = progress, target_dir = target_dir)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -188,7 +188,6 @@
     sha1_url: String = default_sha1_url,
     sha1_version: String = default_sha1_version,
     target_dir: Path = Path.current,
-    verbose: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     /* component */
@@ -227,7 +226,7 @@
           arch_64 = arch_64,
           options = options,
           mingw = mingw,
-          progress = if (verbose) progress else new Progress)
+          progress = if (progress.verbose) progress else new Progress)
       }
     }
 
@@ -415,11 +414,11 @@
 
         val options = getopts(args)
 
-        val progress = new Console_Progress
+        val progress = new Console_Progress(verbose = verbose)
 
         build_polyml(options = options, mingw = mingw, component_name = component_name,
           polyml_url = polyml_url, polyml_version = polyml_version, polyml_name = polyml_name,
           sha1_url = sha1_url, sha1_version = sha1_version, target_dir = target_dir,
-          verbose = verbose, progress = progress)
+          progress = progress)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_spass.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -15,9 +15,9 @@
 
   def build_spass(
     download_url: String = default_download_url,
-    verbose: Boolean = false,
     progress: Progress = new Progress,
-    target_dir: Path = Path.current): Unit = {
+    target_dir: Path = Path.current
+  ): Unit = {
     Isabelle_System.with_tmp_dir("build") { tmp_dir =>
       Isabelle_System.require_command("bison")
       Isabelle_System.require_command("flex")
@@ -85,8 +85,8 @@
       }
 
       Isabelle_System.bash("make", cwd = source_dir.file,
-        progress_stdout = progress.echo_if(verbose, _),
-        progress_stderr = progress.echo_if(verbose, _)).check
+        progress_stdout = progress.echo(_, verbose = true),
+        progress_stderr = progress.echo(_, verbose = true)).check
 
 
       /* install */
@@ -166,9 +166,8 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
-        build_spass(download_url = download_url, verbose = verbose, progress = progress,
-          target_dir = target_dir)
+        build_spass(download_url = download_url, progress = progress, target_dir = target_dir)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -56,7 +56,6 @@
     progress: Progress = new Progress,
     profiles: List[Profile] = default_profiles,
     only_sessions: Set[String] = Set.empty,
-    verbose: Boolean = false,
     target_dir: Path = default_target_dir,
     ml_statistics: Boolean = false,
     image_size: (Int, Int) = default_image_size
@@ -66,8 +65,7 @@
         ML_Statistics.workers_fields).flatMap(_._2).toSet
 
     val data =
-      read_data(options, progress = progress, profiles = profiles,
-        only_sessions = only_sessions, verbose = verbose,
+      read_data(options, progress = progress, profiles = profiles, only_sessions = only_sessions,
         ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain)
 
     present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
@@ -213,8 +211,7 @@
     profiles: List[Profile] = default_profiles,
     only_sessions: Set[String] = Set.empty,
     ml_statistics: Boolean = false,
-    ml_statistics_domain: String => Boolean = _ => true,
-    verbose: Boolean = false
+    ml_statistics_domain: String => Boolean = _ => true
   ): Data = {
     val date = Date.now()
     var data_hosts = Map.empty[String, Set[String]]
@@ -258,7 +255,7 @@
         val Threads_Option = """threads\s*=\s*(\d+)""".r
 
         val sql = profile.select(options, columns, only_sessions)
-        progress.echo_if(verbose, sql)
+        progress.echo(sql, verbose = true)
 
         db.using_statement(sql) { stmt =>
           val res = stmt.execute_query()
@@ -620,9 +617,9 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress
+        val progress = new Console_Progress(verbose = verbose)
 
-        build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
+        build_status(options, progress = progress, only_sessions = only_sessions,
           target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_vampire.scala
--- a/src/Pure/Admin/build_vampire.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_vampire.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -21,7 +21,6 @@
     download_url: String = default_download_url,
     jobs: Int = default_jobs,
     component_name: String = "",
-    verbose: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
@@ -80,14 +79,14 @@
       val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
       val cmake_out =
         progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
-          cwd = source_dir.file, echo = verbose).check.out
+          cwd = source_dir.file, echo = progress.verbose).check.out
 
       val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
       val binary =
         split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
           .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
 
-      progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check
+      progress.bash("make -j" + jobs, cwd = source_dir.file, echo = progress.verbose).check
 
       Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
         platform_dir + Path.basic("vampire").platform_exe)
@@ -151,9 +150,9 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      val progress = new Console_Progress()
+      val progress = new Console_Progress(verbose = verbose)
 
       build_vampire(download_url = download_url, component_name = component_name,
-        jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir)
+        jobs = jobs, progress = progress, target_dir = target_dir)
     })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_verit.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -15,7 +15,6 @@
 
   def build_verit(
     download_url: String = default_download_url,
-    verbose: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current,
     mingw: MinGW = MinGW.none
@@ -75,7 +74,7 @@
         if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
 
       progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
-        cwd = source_dir.file, echo = verbose).check
+        cwd = source_dir.file, echo = progress.verbose).check
 
 
       /* install */
@@ -144,9 +143,9 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
-        build_verit(download_url = download_url, verbose = verbose, progress = progress,
+        build_verit(download_url = download_url, progress = progress,
           target_dir = target_dir, mingw = mingw)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/build_zipperposition.scala
--- a/src/Pure/Admin/build_zipperposition.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -15,7 +15,6 @@
 
   def build_zipperposition(
     version: String = default_version,
-    verbose: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
@@ -43,10 +42,10 @@
       /* build */
 
       progress.echo("OCaml/OPAM setup ...")
-      progress.bash("isabelle ocaml_setup", echo = verbose).check
+      progress.bash("isabelle ocaml_setup", echo = progress.verbose).check
 
       progress.echo("Building Zipperposition for " + platform_name + " ...")
-      progress.bash(cwd = build_dir.file, echo = verbose,
+      progress.bash(cwd = build_dir.file, echo = progress.verbose,
         script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) +
           " zipperposition=" + Bash.string(version)).check
 
@@ -112,9 +111,8 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
-        build_zipperposition(version = version, verbose = verbose, progress = progress,
-          target_dir = target_dir)
+        build_zipperposition(version = version, progress = progress, target_dir = target_dir)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Admin/ci_build.scala
--- a/src/Pure/Admin/ci_build.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Admin/ci_build.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -178,7 +178,7 @@
           selection = config.selection,
           progress = progress,
           clean_build = config.clean,
-          verbose = true,
+          verbose = progress.verbose,
           numa_shuffling = profile.numa,
           max_jobs = profile.jobs,
           dirs = config.include,
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -588,7 +588,7 @@
         progress.interrupt_handler {
           val build_results =
             Build.build(options, selection = Sessions.Selection.session(session),
-              dirs = dirs, progress = progress, verbose = verbose_build)
+              dirs = dirs, progress = progress, verbose = progress.verbose)
           if (!build_results.ok) error("Failed to build session " + quote(session))
 
           if (output_sources.isEmpty && output_pdf.isEmpty) {
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Tools/build_docker.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -39,8 +39,7 @@
     entrypoint: Boolean = false,
     output: Option[Path] = None,
     more_packages: List[String] = Nil,
-    tag: String = "",
-    verbose: Boolean = false
+    tag: String = ""
   ): Unit = {
     val isabelle_name =
       app_archive match {
@@ -103,7 +102,7 @@
             tmp_dir + Path.explode("Isabelle.tar.gz"))
         }
 
-        val quiet_option = if (verbose) "" else " -q"
+        val quiet_option = if (progress.verbose) "" else " -q"
         val tag_option = if_proper(tag, " -t " + Bash.string(tag))
         progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
           echo = true).check
@@ -170,8 +169,10 @@
             case _ => getopts.usage()
           }
 
-        build_docker(new Console_Progress(), app_archive, base = base, work_dir = work_dir,
+        val progress = new Console_Progress(verbose = verbose)
+
+        build_docker(progress, app_archive, base = base, work_dir = work_dir,
           logic = logic, no_build = no_build, entrypoint = entrypoint, output = output,
-          more_packages = more_packages, tag = tag, verbose = verbose)
+          more_packages = more_packages, tag = tag)
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -61,7 +61,6 @@
     version: String = default_version,
     force: Boolean = false,
     dry_run: Boolean = false,
-    verbose: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     check_platform_spec(platform_spec)
@@ -134,7 +133,7 @@
               " -InstallDir " + Bash.string(platform.name) +
               (if (dry_run) " -DryRun" else "") +
               " -NoPath"
-          progress.bash(script, echo = verbose,
+          progress.bash(script, echo = progress.verbose,
             cwd = if (dry_run) null else component_dir.path.file).check
           for (exe <- File.find_files(platform_dir.file, pred = _.getName.endsWith(".exe"))) {
             File.set_executable(File.path(exe), true)
@@ -192,11 +191,11 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
         for (platform <- platforms) {
           dotnet_setup(platform_spec = platform, target_dir = target_dir, install_url = install_url,
-            version = version, force = force, dry_run = dry_run, verbose = verbose, progress = progress)
+            version = version, force = force, dry_run = dry_run, progress = progress)
         }
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -464,7 +464,7 @@
 
         val start_date = Date.now()
 
-        progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
+        progress.echo("Started at " + Build_Log.print_date(start_date), verbose = true)
 
         progress.interrupt_handler {
           dump(options, logic,
@@ -486,7 +486,7 @@
         val end_date = Date.now()
         val timing = end_date.time - start_date.time
 
-        progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
+        progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
         progress.echo(timing.message_hms + " elapsed time")
       })
 }
diff -r 3bc49507bae5 -r f5d6cd98b16a src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Sat Mar 04 23:25:30 2023 +0100
@@ -275,7 +275,7 @@
 
   /* original repository clones and patches */
 
-  def vscodium_patch(verbose: Boolean = false, progress: Progress = new Progress): String = {
+  def vscodium_patch(progress: Progress = new Progress): String = {
     val platform_info = linux_platform_info
     check_system(List(platform_info.platform))
 
@@ -291,7 +291,7 @@
             "./prepare_vscode.sh",
             // enforce binary diff of code.xpm
             "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm"
-          ).mkString("\n"), cwd = build_dir.file, echo = verbose).check
+          ).mkString("\n"), cwd = build_dir.file, echo = progress.verbose).check
         Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base,
           diff_options = "--exclude=.git --exclude=node_modules")
       }
@@ -306,7 +306,6 @@
   def build_vscodium(
     target_dir: Path = Path.current,
     platforms: List[Platform.Family.Value] = default_platforms,
-    verbose: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     check_system(platforms)
@@ -328,7 +327,7 @@
     def write_patch(name: String, patch: String): Unit =
       File.write(patches_dir + Path.explode(name).patch, patch)
 
-    write_patch("01-vscodium", vscodium_patch(verbose = verbose, progress = progress))
+    write_patch("01-vscodium", vscodium_patch(progress = progress))
 
 
     /* build */
@@ -346,7 +345,7 @@
 
         progress.echo("Build ...")
         progress.bash(platform_info.environment + "\n" + "./build.sh",
-          cwd = build_dir.file, echo = verbose).check
+          cwd = build_dir.file, echo = progress.verbose).check
 
         if (platform_info.primary) {
           Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
@@ -432,10 +431,9 @@
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
-        val progress = new Console_Progress()
+        val progress = new Console_Progress(verbose = verbose)
 
-        build_vscodium(target_dir = target_dir, platforms = platforms,
-          verbose = verbose, progress = progress)
+        build_vscodium(target_dir = target_dir, platforms = platforms, progress = progress)
       })
 
   val isabelle_tool2 =