# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1738963161 -3600
# Node ID 343cf88b0eefe38da40ea8c6c064c774c78334c6
# Parent  80b00abb9aac333e4043ba767c1b61f1bf8dc87e
clarified;

diff -r 80b00abb9aac -r 343cf88b0eef src/Tools/Find_Facts/src/elm.scala
--- a/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 22:18:44 2025 +0100
+++ b/src/Tools/Find_Facts/src/elm.scala	Fri Feb 07 22:19:21 2025 +0100
@@ -35,6 +35,16 @@
       if (!main_file.is_file) error("Main elm file does not exist: " + main_file)
       new Project(name, dir, main, head)
     }
+
+    def get_digest(output_file: Path): SHA1.Digest =
+      Exn.capture {
+        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 {
+        case Exn.Res(s) => SHA1.fake_digest(s)
+        case _ => SHA1.digest_empty
+      }
   }
 
   class Project private(name: String, dir: Path, main: Path, head: XML.Body) {
@@ -58,19 +68,9 @@
       meta_info ::: head_digest ::: source_digest
     }
 
-    def get_digest(output_file: Path): SHA1.Digest =
-      Exn.capture {
-        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 {
-        case Exn.Res(s) => SHA1.fake_digest(s)
-        case _ => SHA1.digest_empty
-      }
-
     def build_html(output_file: Path, progress: Progress = new Progress): Unit = {
       val digest = sources_shasum.digest
-      if (digest != get_digest(output_file)) {
+      if (digest != Project.get_digest(output_file)) {
         progress.echo("Building web application " + output_file.absolute + " ...")
 
         val cmd =