# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737553406 -3600
# Node ID a70e471b25825f76ea59c6da380d8acb5cd7cace
# Parent  794591b2ea97f76b665454276701880bc7dbf04f
tuned messages;

diff -r 794591b2ea97 -r a70e471b2582 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Wed Jan 22 11:23:35 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Wed Jan 22 14:43:26 2025 +0100
@@ -619,6 +619,7 @@
 
     if (sessions.isEmpty) progress.echo("Nothing to index")
     else {
+      val start_date = Date.now()
       val stats =
         using(solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
           using(Export.open_database_context(store)) { database_context =>
@@ -635,7 +636,7 @@
                   Build.read_theory(theory_context) match {
                     case None => progress.echo_warning("No snapshot for theory " + name.theory)
                     case Some(snapshot) =>
-                      progress.echo("Theory " + name.theory + " ...")
+                      progress.echo("Indexing theory " + quote(name.theory), verbose = true)
                       val blocks =
                         make_thy_blocks(options, session, browser_info_context, document_info,
                           theory_context, snapshot, info.chapter)
@@ -652,8 +653,9 @@
           Find_Facts.query_stats(db, query)
         }
 
-      progress.echo("Indexed " + stats.results + " blocks with " +
-        stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
+      val timing = Date.now() - start_date
+      progress.echo("Indexed " + stats.results + " blocks with " + stats.consts + " consts, " +
+        stats.typs + " typs, " + stats.thms + " thms in " + timing.message)
     }
   }