# 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 = {