# HG changeset patch # User wenzelm # Date 1736718056 -3600 # Node ID b1b87d078161353a76a7d46da518671c2ce7468c # Parent 353db84fa71bf1ea267bc97923c6dd10fec3b785 tuned messages: more verbosity; diff -r 353db84fa71b -r b1b87d078161 src/Tools/Find_Facts/src/find_facts.scala --- a/src/Tools/Find_Facts/src/find_facts.scala Sun Jan 12 22:16:17 2025 +0100 +++ b/src/Tools/Find_Facts/src/find_facts.scala Sun Jan 12 22:40:56 2025 +0100 @@ -642,6 +642,7 @@ val dirs_buffer = new mutable.ListBuffer[Path] var no_build = false var options = Options.init() + var verbose = false val getopts = Getopts(""" Usage: isabelle find_facts_index [OPTIONS] [SESSIONS ...] @@ -651,26 +652,28 @@ -d DIR include session directory -n no build -- take existing session build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -v verbose build - Index sessions for find_facts. + Build and index sessions for Find_Facts. """, "c" -> (_ => clean = true), "d:" -> (arg => dirs_buffer += Path.explode(arg)), "n" -> (_ => no_build = true), - "o:" -> (arg => options = options + arg)) + "o:" -> (arg => options = options + arg), + "v" -> (_ => verbose = true)) val sessions = getopts(args) val dirs = dirs_buffer.toList - val progress = new Console_Progress() + val progress = new Console_Progress(verbose = verbose) /* build */ if (!no_build) { def build(test: Boolean = false): Build.Results = - Build.build(options, selection = Sessions.Selection(sessions = sessions), - no_build = test, dirs = dirs) + Build.build(options, selection = Sessions.Selection(sessions = sessions), dirs = dirs, + no_build = test, progress = if (test) new Progress else progress) progress.interrupt_handler { if (!build(test = true).ok) {