--- 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 " +
--- 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 = {