tuned messages: more verbosity;
authorwenzelm
Sun, 12 Jan 2025 22:40:56 +0100
changeset 81801 b1b87d078161
parent 81800 353db84fa71b
child 81802 4d78ad5abeca
tuned messages: more verbosity;
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) {