# HG changeset patch # User Fabian Huch # 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 =