# HG changeset patch
# User wenzelm
# Date 1693750686 -7200
# Node ID 9a5d86549719bb731a3a66d8147f4f959f3c9507
# Parent  163c392675dcf3e9cad74f02d5d0aee2e87ff4a3
support "isabelle build_worker -q";

diff -r 163c392675dc -r 9a5d86549719 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Sep 03 13:38:56 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Sep 03 16:18:06 2023 +0200
@@ -587,6 +587,7 @@
     isabelle_home: Path = Path.current,
     afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
+    quiet: Boolean = false,
     verbose: Boolean = false
   ): String = {
     val options =
@@ -597,6 +598,7 @@
       dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
       if_proper(host.numa, " -N") + " -j" + host.jobs +
       options.map(opt => " -o " + Bash.string(opt.print)).mkString +
+      if_proper(quiet, " -q") +
       if_proper(verbose, " -v")
   }
 
@@ -649,6 +651,7 @@
           List(
             Options.Spec.make("build_database_server"),
             Options.Spec.make("build_database")))
+      var quiet = false
       var verbose = false
 
       val getopts = Getopts("""
@@ -661,6 +664,7 @@
     -d DIR       include session directory
     -j INT       maximum number of parallel jobs (default 1)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -q           quiet mode: no progress
     -v           verbose
 """,
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
@@ -669,12 +673,16 @@
         "d:" -> (arg => dirs += Path.explode(arg)),
         "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
         "o:" -> (arg => options = options + arg),
+        "q" -> (_ => quiet = true),
         "v" -> (_ => verbose = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      val progress = new Console_Progress(verbose = verbose)
+      val progress =
+        if (quiet && verbose) new Progress { override def verbose: Boolean = true }
+        else if (quiet) new Progress
+        else new Console_Progress(verbose = verbose)
 
       val results =
         progress.interrupt_handler {