clarified;
authorFabian Huch <huch@in.tum.de>
Fri, 07 Feb 2025 20:31:52 +0100
changeset 82110 9b4e021cfd08
parent 82109 28ef95b041f0
child 82111 80b00abb9aac
clarified;
src/Tools/Find_Facts/src/elm.scala
--- a/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 20:30:13 2025 +0100
+++ b/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 20:31:52 2025 +0100
@@ -59,9 +59,9 @@
       meta_info ::: head_digest ::: source_digest
     }
 
-    def get_digest: SHA1.Digest =
+    def get_digest(file: Path = output_file): SHA1.Digest =
       Exn.capture {
-        val html = HTML.parse_document(File.read(output_file))
+        val html = HTML.parse_document(File.read(file))
         val elem = html.head.getElementsByTag("meta").attr("name", "shasum")
         Library.the_single(elem.eachAttr("content").asScala.toList)
       } match {
@@ -71,7 +71,7 @@
 
     def build_html(progress: Progress = new Progress): String = {
       val digest = sources_shasum.digest
-      if (digest == get_digest) File.read(output_file)
+      if (digest == get_digest()) File.read(output_file)
       else {
         progress.echo("Building web application " + output_file.absolute + " ...")