# HG changeset patch
# User wenzelm
# Date 1736715922 -3600
# Node ID 150651b9d2a23efab067d9a1d25925b64548369b
# Parent  a0ecb9d0666477b32232e2ceeaef14c54893817c
tuned messages;

diff -r a0ecb9d06664 -r 150651b9d2a2 src/Tools/Find_Facts/src/elm.scala
--- a/src/Tools/Find_Facts/src/elm.scala	Sun Jan 12 21:45:49 2025 +0100
+++ b/src/Tools/Find_Facts/src/elm.scala	Sun Jan 12 22:05:22 2025 +0100
@@ -68,7 +68,7 @@
       val digest = sources_shasum.digest
       if (digest == get_digest) File.read(output)
       else {
-        progress.echo_warning("Building web application in " + output.absolute + " ...")
+        progress.echo("Building web application " + output.absolute + " ...")
 
         val cmd =
           File.bash_path(Path.explode("$ISABELLE_ELM_HOME/elm")) + " make " +
diff -r a0ecb9d06664 -r 150651b9d2a2 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 21:45:49 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 22:05:22 2025 +0100
@@ -853,7 +853,6 @@
     web_dir: Path = default_web_dir,
     progress: Progress = new Progress
   ): Unit = {
-    progress.echo("Web directory " + web_dir.expand)
     Isabelle_System.copy_dir(template_web_dir, web_dir, direct = true)
 
     val database = options.string("find_facts_database_name")
@@ -876,7 +875,7 @@
 
     using(Solr.open_database(database)) { db =>
       val stats = Find_Facts.query_stats(db, Query(Nil))
-      progress.echo("Started find facts with " + stats.results + " blocks, " +
+      progress.echo("Started Find_Facts with " + stats.results + " blocks, " +
         stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
 
       val server =
@@ -913,7 +912,7 @@
           }))
 
       server.start()
-      progress.echo("Server started on port " + server.http_server.getAddress.getPort)
+      progress.echo("Server started " + server.toString + "/app")
 
       @tailrec
       def loop(): Unit = {