# HG changeset patch
# User wenzelm
# Date 1736693910 -3600
# Node ID e08eab19cdeb6acf28b5af46c2c80c090276a788
# Parent  bd24acc5162cd690fc7bc1d42ccd1473f2872de5
clarified signature: progress is usually optional;

diff -r bd24acc5162c -r e08eab19cdeb src/Tools/Find_Facts/src/elm.scala
--- a/src/Tools/Find_Facts/src/elm.scala	Sun Jan 12 15:54:32 2025 +0100
+++ b/src/Tools/Find_Facts/src/elm.scala	Sun Jan 12 15:58:30 2025 +0100
@@ -64,7 +64,7 @@
         case _ => SHA1.digest_empty
       }
 
-    def build_html(progress: Progress): String = {
+    def build_html(progress: Progress = new Progress): String = {
       val digest = sources_shasum.digest
       if (digest == get_digest) File.read(output)
       else {
diff -r bd24acc5162c -r e08eab19cdeb src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 15:54:32 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 15:58:30 2025 +0100
@@ -836,7 +836,7 @@
       HTML.script_file(
         "https://unpkg.com/material-components-web-elm@9.1.0/dist/material-components-web-elm.min.js")))
 
-    val frontend = project.build_html(progress)
+    val frontend = project.build_html(progress = progress)
 
     using(Solr.open_database(database)) { db =>
       val stats = Find_Facts.query_stats(db, Query(Nil))
@@ -852,7 +852,8 @@
           },
           new HTTP.Service("app") {
             def apply(request: HTTP.Request): Option[HTTP.Response] =
-              Some(HTTP.Response.html(if (devel) project.build_html(progress) else frontend))
+              Some(HTTP.Response.html(
+                if (devel) project.build_html(progress = progress) else frontend))
           },
           new HTTP.REST_Service("api/block", progress = progress) {
             def handle(body: JSON.T): Option[JSON.T] =