# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1738963124 -3600
# Node ID 80b00abb9aac333e4043ba767c1b61f1bf8dc87e
# Parent  9b4e021cfd08684359c05e463fc3f7649291b88d
clarified output file;

diff -r 9b4e021cfd08 -r 80b00abb9aac src/Tools/Find_Facts/src/elm.scala
--- a/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 20:31:52 2025 +0100
+++ b/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 22:18:44 2025 +0100
@@ -28,17 +28,16 @@
       name: String,
       dir: Path,
       main: Path = Path.explode("src/Main.elm"),
-      output_file: Path = Path.explode("index.html"),
       head: XML.Body = Nil
     ): Project = {
       if (!dir.is_dir) error("Project directory does not exist: " + dir)
       val main_file = dir + main
       if (!main_file.is_file) error("Main elm file does not exist: " + main_file)
-      new Project(name, dir, main, dir + output_file, head)
+      new Project(name, dir, main, head)
     }
   }
 
-  class Project private(name: String, dir: Path, main: Path, output_file: Path, head: XML.Body) {
+  class Project private(name: String, dir: Path, main: Path, head: XML.Body) {
     val definition = JSON.parse(File.read(dir + Path.basic("elm.json")))
     val src_dirs =
       JSON.strings(definition, "source-directories").getOrElse(
@@ -59,9 +58,9 @@
       meta_info ::: head_digest ::: source_digest
     }
 
-    def get_digest(file: Path = output_file): SHA1.Digest =
+    def get_digest(output_file: Path): SHA1.Digest =
       Exn.capture {
-        val html = HTML.parse_document(File.read(file))
+        val html = HTML.parse_document(File.read(output_file))
         val elem = html.head.getElementsByTag("meta").attr("name", "shasum")
         Library.the_single(elem.eachAttr("content").asScala.toList)
       } match {
@@ -69,10 +68,9 @@
         case _ => SHA1.digest_empty
       }
 
-    def build_html(progress: Progress = new Progress): String = {
+    def build_html(output_file: Path, progress: Progress = new Progress): Unit = {
       val digest = sources_shasum.digest
-      if (digest == get_digest()) File.read(output_file)
-      else {
+      if (digest != get_digest(output_file)) {
         progress.echo("Building web application " + output_file.absolute + " ...")
 
         val cmd =
@@ -91,8 +89,6 @@
         file.head.append(XML.string_of_body(head))
         val html = file.html
         File.write(output_file, html)
-
-        html
       }
     }
   }
diff -r 9b4e021cfd08 -r 80b00abb9aac src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Fri Feb 07 20:31:52 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Feb 07 22:18:44 2025 +0100
@@ -885,10 +885,16 @@
 
   /* web */
 
+  val web_html: Path = Path.basic("index").html
+
   val web_sources: Path = Path.explode("$FIND_FACTS_HOME/web")
   val default_web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web")
 
-  def build_html(web_dir: Path = default_web_dir, progress: Progress = new Progress): String = {
+  def build_html(
+    output_file: Path,
+    web_dir: Path = default_web_dir,
+    progress: Progress = new Progress
+  ): Unit = {
     Isabelle_System.copy_dir(web_sources, web_dir, direct = true)
     val logo = Bytes.read(web_dir + Path.explode("favicon.ico"))
     val project =
@@ -902,7 +908,7 @@
             "https://unpkg.com/material-components-web-elm@9.1.0/dist/material-components-web-elm.min.css"),
           HTML.script_file(
             "https://unpkg.com/material-components-web-elm@9.1.0/dist/material-components-web-elm.min.js")))
-    project.build_html(progress = progress)
+    project.build_html(output_file, progress = progress)
   }
 
 
@@ -917,7 +923,12 @@
     val database = options.string("find_facts_database_name")
     val encode = new Encode(options)
 
-    val html = build_html(progress = progress)
+    def rebuild(): String = {
+      build_html(default_web_dir + web_html, progress = progress)
+      File.read(default_web_dir + web_html)
+    }
+
+    val html = rebuild()
 
     val solr = Solr.init(solr_data_dir)
     resolve_indexes(solr)
@@ -933,7 +944,7 @@
           HTTP.CSS_Service,
           new HTTP.Service("find_facts") {
             def apply(request: HTTP.Request): Option[HTTP.Response] =
-              Some(HTTP.Response.html(if (devel) build_html(progress = progress) else html))
+              Some(HTTP.Response.html(if (devel) rebuild() else html))
           },
           new HTTP.REST_Service("api/block", progress = progress) {
             def handle(body: JSON.T): Option[JSON.T] =