# HG changeset patch
# User wenzelm
# Date 1678030578 -3600
# Node ID 5642de4d225d568cf961fb8edec7790ac715fbc1
# Parent  84aa349ed5976cd33cfea2134ebab903c5bc4a06
clarified signature: manage "verbose" flag via "progress";

diff -r 84aa349ed597 -r 5642de4d225d src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -51,8 +51,7 @@
     val build_results0 =
       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 = progress.verbose)
+        select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs)
 
     if (build_results0.ok) {
       val build_options =
@@ -95,8 +94,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 = progress.verbose,
-        session_setup = session_setup)
+        numa_shuffling = numa_shuffling, max_jobs = max_jobs, session_setup = session_setup)
     }
     else build_results0
   }
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Admin/ci_build.scala
--- a/src/Pure/Admin/ci_build.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Admin/ci_build.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -178,7 +178,6 @@
           selection = config.selection,
           progress = progress,
           clean_build = config.clean,
-          verbose = progress.verbose,
           numa_shuffling = profile.numa,
           max_jobs = profile.jobs,
           dirs = config.include,
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Thy/browser_info.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -549,7 +549,6 @@
     context: Context,
     session_context: Export.Session_Context,
     progress: Progress = new Progress,
-    verbose: Boolean = false,
   ): Unit = {
     progress.expose_interrupt()
 
@@ -580,7 +579,7 @@
           error("Illegal document variant " + quote(doc.name) +
             " (conflict with " + session_graph_path + ")")
         }
-        if (verbose) progress.echo("Presenting document " + session_name + "/" + doc.name)
+        progress.echo("Presenting document " + session_name + "/" + doc.name, verbose = true)
         if (session_info.document_echo) progress.echo("Document at " + doc_path)
         Bytes.write(doc_path, document.pdf)
         doc
@@ -602,7 +601,7 @@
       val snapshot = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err()
       val theory = context.theory_by_name(session_name, theory_name) getOrElse err()
 
-      if (verbose) progress.echo("Presenting theory " + quote(theory_name))
+      progress.echo("Presenting theory " + quote(theory_name), verbose = true)
 
       val thy_elements = theory.elements(context.elements)
 
@@ -626,7 +625,7 @@
           progress.expose_interrupt()
 
           val file = blob_name.node
-          if (verbose) progress.echo("Presenting file " + quote(file))
+          progress.echo("Presenting file " + quote(file), verbose = true)
 
           val file_html = session_dir + context.file_html(file)
           val file_dir = file_html.dir
@@ -672,8 +671,7 @@
     store: Sessions.Store,
     deps: Sessions.Deps,
     sessions: List[String],
-    progress: Progress = new Progress,
-    verbose: Boolean = false
+    progress: Progress = new Progress
   ): Unit = {
     val root_dir = browser_info.presentation_dir(store).absolute
     progress.echo("Presentation in " + root_dir)
@@ -701,7 +699,7 @@
 
       Par_List.map({ (session: String) =>
         using(database_context.open_session(deps.background(session))) { session_context =>
-          build_session(context1, session_context, progress = progress, verbose = verbose)
+          build_session(context1, session_context, progress = progress)
         }
       }, sessions1)
     }
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -586,7 +586,7 @@
         progress.interrupt_handler {
           val build_results =
             Build.build(options, selection = Sessions.Selection.session(session),
-              dirs = dirs, progress = progress, verbose = progress.verbose)
+              dirs = dirs, progress = progress)
           if (!build_results.ok) error("Failed to build session " + quote(session))
 
           if (output_sources.isEmpty && output_pdf.isEmpty) {
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -306,7 +306,6 @@
   def deps(sessions_structure: Structure,
     progress: Progress = new Progress,
     inlined_files: Boolean = false,
-    verbose: Boolean = false,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty
   ): Deps = {
@@ -340,10 +339,10 @@
               Background(base = deps_base, sessions_structure = sessions_structure)
             val resources = new Resources(session_background)
 
-            if (verbose || list_files) {
-              val groups = if_proper(info.groups, info.groups.mkString(" (", " ", ")"))
-              progress.echo("Session " + info.chapter + "/" + session_name + groups)
-            }
+            progress.echo(
+              "Session " + info.chapter + "/" + session_name +
+                if_proper(info.groups, info.groups.mkString(" (", " ", ")")),
+              verbose = !list_files)
 
             val dependencies = resources.session_dependencies(info)
 
@@ -972,12 +971,11 @@
       selection: Selection,
       progress: Progress = new Progress,
       loading_sessions: Boolean = false,
-      inlined_files: Boolean = false,
-      verbose: Boolean = false
+      inlined_files: Boolean = false
     ): Deps = {
       val deps =
         Sessions.deps(sessions_structure.selection(selection),
-          progress = progress, inlined_files = inlined_files, verbose = verbose)
+          progress = progress, inlined_files = inlined_files)
 
       if (loading_sessions) {
         val selection_size = deps.sessions_structure.build_graph.size
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -79,7 +79,6 @@
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
-    verbose: Boolean = false,
     export_files: Boolean = false,
     augment_options: String => List[Options.Spec] = _ => Nil,
     session_setup: (String, Session) => Unit = (_, _) => ()
@@ -104,8 +103,7 @@
 
     val build_deps = {
       val deps0 =
-        Sessions.deps(full_sessions.selection(selection),
-          progress = progress, inlined_files = true, verbose = verbose,
+        Sessions.deps(full_sessions.selection(selection), progress = progress, inlined_files = true,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
@@ -151,8 +149,7 @@
       Build_Process.Context(store, build_deps, progress = progress,
         hostname = Isabelle_System.hostname(build_options.string("build_hostname")),
         build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
-        fresh_build = fresh_build, no_build = no_build, verbose = verbose,
-        session_setup = session_setup)
+        fresh_build = fresh_build, no_build = no_build, session_setup = session_setup)
 
     store.prepare_output_dir()
 
@@ -182,7 +179,7 @@
           progress.echo("Exporting " + info.name + " ...")
           for ((dir, prune, pats) <- info.export_files) {
             Export.export_files(store, name, info.dir + dir,
-              progress = if (verbose) progress else new Progress,
+              progress = if (progress.verbose) progress else new Progress,
               export_prune = prune,
               export_patterns = pats)
           }
@@ -194,10 +191,10 @@
       results.sessions_ok.filter(name => browser_info.enabled(results.info(name)))
     if (presentation_sessions.nonEmpty && !progress.stopped) {
       Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions,
-        progress = progress, verbose = verbose)
+        progress = progress)
     }
 
-    if (!results.ok && (verbose || !no_build)) {
+    if (!results.ok && (progress.verbose || !no_build)) {
       progress.echo("Unfinished session(s): " + commas(results.unfinished))
     }
 
@@ -291,13 +288,12 @@
 
       val start_date = Date.now()
 
-      if (verbose) {
-        val hostname = Isabelle_System.hostname(options.string("build_hostname"))
-        progress.echo(
-          "Started at " + Build_Log.print_date(start_date) +
-            " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + hostname +")")
-        progress.echo(Build_Log.Settings.show() + "\n")
-      }
+      val hostname = Isabelle_System.hostname(options.string("build_hostname"))
+      progress.echo(
+        "Started at " + Build_Log.print_date(start_date) +
+          " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + hostname +")",
+        verbose = true)
+      progress.echo(Build_Log.Settings.show() + "\n", verbose = true)
 
       val results =
         progress.interrupt_handler {
@@ -324,15 +320,12 @@
             fresh_build = fresh_build,
             no_build = no_build,
             soft_build = soft_build,
-            verbose = verbose,
             export_files = export_files)
         }
       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 84aa349ed597 -r 5642de4d225d src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -114,7 +114,6 @@
     override val node_info: Host.Node_Info
   ) extends Build_Job {
     private val store = build_context.store
-    private val verbose = build_context.verbose
 
     def session_name: String = session_background.session_name
     def job_name: String = session_name
@@ -505,13 +504,12 @@
         process_result.err_lines.foreach(progress.echo(_))
 
         if (process_result.ok) {
-          if (verbose) {
-            val props = build_log.session_timing
-            val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
-            val timing = Markup.Timing_Properties.get(props)
-            progress.echo(
-              "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")")
-          }
+          val props = build_log.session_timing
+          val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
+          val timing = Markup.Timing_Properties.get(props)
+          progress.echo(
+            "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")",
+            verbose = true)
           progress.echo(
             "Finished " + session_name + " (" + process_result.timing.message_resources + ")")
         }
@@ -613,7 +611,6 @@
     theories: List[String] = Nil,
     message_head: List[Regex] = Nil,
     message_body: List[Regex] = Nil,
-    verbose: Boolean = false,
     progress: Progress = new Progress,
     margin: Double = Pretty.default_margin,
     breakgain: Double = Pretty.default_breakgain,
@@ -657,7 +654,7 @@
                   val rendering = new Rendering(snapshot, options, session)
                   val messages =
                     rendering.text_messages(Text.Range.full)
-                      .filter(message => verbose || Protocol.is_exported(message.info))
+                      .filter(message => progress.verbose || Protocol.is_exported(message.info))
                   if (messages.nonEmpty) {
                     val line_document = Line.Document(snapshot.node.source)
                     val buffer = new mutable.ListBuffer[String]
@@ -747,12 +744,12 @@
 
       val sessions = getopts(args)
 
-      val progress = new Console_Progress()
+      val progress = new Console_Progress(verbose = verbose)
 
       if (sessions.isEmpty) progress.echo_warning("No sessions to print")
       else {
         print_log(options, sessions, theories = theories, message_head = message_head,
-          message_body = message_body, verbose = verbose, margin = margin, progress = progress,
+          message_body = message_body, margin = margin, progress = progress,
           unicode_symbols = unicode_symbols)
       }
     })
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -27,7 +27,6 @@
       max_jobs: Int = 1,
       fresh_build: Boolean = false,
       no_build: Boolean = false,
-      verbose: Boolean = false,
       session_setup: (String, Session) => Unit = (_, _) => (),
       uuid: String = UUID.random().toString
     ): Context = {
@@ -83,7 +82,7 @@
       val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
       new Context(store, build_deps, sessions, ordering, hostname, numa_nodes,
         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
-        no_build = no_build, verbose = verbose, session_setup, uuid = uuid)
+        no_build = no_build, session_setup, uuid = uuid)
     }
   }
 
@@ -99,7 +98,6 @@
     val max_jobs: Int,
     val fresh_build: Boolean,
     val no_build: Boolean,
-    val verbose: Boolean,
     val session_setup: (String, Session) => Unit,
     val uuid: String
   ) {
@@ -608,7 +606,6 @@
   protected val store: Sessions.Store = build_context.store
   protected val build_options: Options = store.options
   protected val build_deps: Sessions.Deps = build_context.build_deps
-  protected val verbose: Boolean = build_context.verbose
 
 
   /* global state: internal var vs. external database */
@@ -725,7 +722,7 @@
         .make_result(session_name, Process_Result.ok, output_shasum, current = true)
     }
     else if (build_context.no_build) {
-      progress.echo_if(verbose, "Skipping " + session_name + " ...")
+      progress.echo("Skipping " + session_name + " ...", verbose = true)
       state.
         remove_pending(session_name).
         make_result(session_name, Process_Result.error, output_shasum)
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Tools/server_commands.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -74,8 +74,7 @@
           progress = progress,
           build_heap = true,
           dirs = dirs,
-          infos = session_background.infos,
-          verbose = progress.verbose)
+          infos = session_background.infos)
 
       val sessions_order =
         session_background.sessions_structure.imports_topological_order.zipWithIndex.
diff -r 84aa349ed597 -r 5642de4d225d src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -54,8 +54,7 @@
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     fresh_build: Boolean = false,
-    no_build: Boolean = false,
-    verbose: Boolean = false
+    no_build: Boolean = false
   ): Build.Results = {
     /* excluded sessions */
 
@@ -80,7 +79,7 @@
       Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
         selection = selection, build_heap = build_heap, clean_build = clean_build,
         numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
-        no_build = no_build, verbose = verbose, augment_options = augment_options)
+        no_build = no_build, augment_options = augment_options)
 
     val store = build_results.store
     val sessions_structure = build_results.deps.sessions_structure
@@ -223,8 +222,7 @@
               numa_shuffling = Host.numa_check(progress, numa_shuffling),
               max_jobs = max_jobs,
               fresh_build,
-              no_build = no_build,
-              verbose = verbose)
+              no_build = no_build)
           }
 
         sys.exit(results.rc)