# HG changeset patch # User Fabian Huch # Date 1738963404 -3600 # Node ID b636cad7b684be1ab8d315f784f0807fd70594d3 # Parent 343cf88b0eefe38da40ea8c6c064c774c78334c6 web component for Find_Facts: bundled assets and compiled elm app; diff -r 343cf88b0eef -r b636cad7b684 etc/build.props --- a/etc/build.props Fri Feb 07 22:19:21 2025 +0100 +++ b/etc/build.props Fri Feb 07 22:23:24 2025 +0100 @@ -25,6 +25,7 @@ src/Pure/Admin/component_easychair.scala \ src/Pure/Admin/component_elm.scala \ src/Pure/Admin/component_eptcs.scala \ + src/Pure/Admin/component_find_facts_web.scala \ src/Pure/Admin/component_flatlaf.scala \ src/Pure/Admin/component_foiltex.scala \ src/Pure/Admin/component_fonts.scala \ diff -r 343cf88b0eef -r b636cad7b684 src/Pure/Admin/component_find_facts_web.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/component_find_facts_web.scala Fri Feb 07 22:23:24 2025 +0100 @@ -0,0 +1,152 @@ +/* Title: Pure/Admin/component_find_facts_web.scala + Author: Fabian Huch, TU Muenchen + +Build Isabelle component for find_facts web app, including external resources. +*/ + +package isabelle + + +import find_facts.Find_Facts + + +object Component_Find_Facts_Web { + /* roboto font */ + + val default_roboto_url = "https://r2.fontsource.org/fonts/roboto" + val default_roboto_version = "5.1.1" + + + /* material components web elm */ + + val default_mcwe_url = "https://unpkg.com/material-components-web-elm" + val default_mcwe_version = "9.1.0" + + + /* build find facts web app */ + + def build_find_facts_web( + roboto_base_url: String = default_roboto_url, + roboto_version: String = default_roboto_version, + mcwe_base_url: String = default_mcwe_url, + mcwe_version: String = default_mcwe_version, + target_dir: Path = Path.current, + progress: Progress = new Progress, + ): Unit = { + /* component */ + + val component_name = "find_facts_web-" + Date.Format.alt_date(Date.now()) + val component_dir = + Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) + + val web_dir = Isabelle_System.make_directory(component_dir.path + Path.basic("web")) + + + /* roboto */ + + val roboto_download = roboto_base_url + "@" + roboto_version + "/download.zip" + val roboto_fonts = + List(300, 400, 500).map(weight => weight -> ("roboto-latin-" + weight + "-normal.woff")) + + Isabelle_System.with_tmp_dir("download") { download_dir => + val archive_path = download_dir + Path.basic("download.zip") + + Isabelle_System.download_file(roboto_download, archive_path) + Isabelle_System.extract(archive_path, download_dir) + + roboto_fonts.foreach((_, name) => + Isabelle_System.copy_file(download_dir + Path.make(List("webfonts", name)), web_dir)) + Isabelle_System.copy_file( + download_dir + Path.basic("LICENSE"), + component_dir.path + Path.basic("LICENSE-roboto")) + + File.write(web_dir + Path.basic("roboto.css"), roboto_fonts.map((weight, name) => """ +@font-face { + font-family: 'Roboto'; + font-weight: """ + weight + """; + src: url('./""" + name + """') format('woff'); +} +""").mkString) + } + + val roboto_css = "roboto.css" -> HTTP.Content.mime_type_css + val roboto_assets = roboto_css :: roboto_fonts.map((_, name) => name -> "font/woff") + + + /* mcwe */ + + def mcwe_file(path: String): String = mcwe_base_url + "@" + mcwe_version + "/" + path + + val mcwe_assets = + List( + "material-components-web-elm.min.js" -> HTTP.Content.mime_type_js, + "material-components-web-elm.min.css" -> HTTP.Content.mime_type_css) + + for ((name, _) <- mcwe_assets) + Isabelle_System.download_file(mcwe_file("dist/" + name), web_dir + Path.basic(name)) + + + /* settings */ + + val assets = + (roboto_assets ::: mcwe_assets).map((name, mime_type) => name + ":" + mime_type).mkString(",") + component_dir.write_settings(""" +FIND_FACTS_WEB_ASSETS_DIR="$COMPONENT/web" +FIND_FACTS_WEB_ASSETS="""" + assets + """" +""") + + /* README */ + + File.write(component_dir.README, + """This component contains web assets (downloaded from recommended CDNs) for the Find_Facts +web application, and its compiled index.html. + +Sources can be found in $FIND_FACTS_HOME/web. + + Fabian Huch +""") + + + /* pre-compiled web app */ + + Isabelle_System.with_tmp_dir("find_facts") { dir => + Find_Facts.build_html(web_dir + Find_Facts.web_html, dir, assets, progress = progress) + } + + + /* license */ + + File.write( + component_dir.path + Path.basic("LICENSE-material-components-web-elm"), + Url.read(mcwe_file("LICENSE"))) + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool( + "component_find_facts_web", + "build Find_Facts web component from elm sources and external resources", + Scala_Project.here, + { args => + var target_dir = Path.current + + val getopts = Getopts(""" +Usage: isabelle component_find_facts_web [OPTIONS] + + Options are: + -D DIR target directory (default ".") + + Build Find_Facts web component from the specified url and elm sources. +""", + "D:" -> (arg => target_dir = Path.explode(arg))) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val progress = new Console_Progress() + + build_find_facts_web(target_dir = target_dir, progress = progress) + }) +} \ No newline at end of file diff -r 343cf88b0eef -r b636cad7b684 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri Feb 07 22:19:21 2025 +0100 +++ b/src/Pure/System/isabelle_tool.scala Fri Feb 07 22:23:24 2025 +0100 @@ -178,6 +178,7 @@ Component_EPTCS.isabelle_tool, Component_Easychair.isabelle_tool, Component_Elm.isabelle_tool, + Component_Find_Facts_Web.isabelle_tool, Component_FlatLaf.isabelle_tool, Component_Foiltex.isabelle_tool, Component_Fonts.isabelle_tool, diff -r 343cf88b0eef -r b636cad7b684 src/Tools/Find_Facts/src/find_facts.scala --- a/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 07 22:19:21 2025 +0100 +++ b/src/Tools/Find_Facts/src/find_facts.scala Fri Feb 07 22:23:24 2025 +0100 @@ -887,28 +887,58 @@ val web_html: Path = Path.basic("index").html - val web_sources: Path = Path.explode("$FIND_FACTS_HOME/web") + val web_sources_dir: Path = Path.explode("$FIND_FACTS_HOME/web") + val web_assets_dir: Path = Path.explode("$FIND_FACTS_WEB_ASSETS_DIR") + + val default_web_assets: String = Isabelle_System.getenv("FIND_FACTS_WEB_ASSETS") val default_web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web") + def web_project(dir: Path, web_assets: String = default_web_assets): Elm.Project = { + val logo = Bytes.read(web_sources_dir + Path.explode("favicon.ico")) + + val assets = space_explode(',', web_assets).map(Asset.parse) + val css = + for ((asset, mime_type) <- assets if mime_type == HTTP.Content.mime_type_css) + yield HTML.style_file("find_facts/" + asset) + val js = + for ((asset, mime_type) <- assets if mime_type == HTTP.Content.mime_type_js) + yield HTML.script_file("find_facts/" + asset) + + Elm.Project("Find_Facts", dir, head = + HTML.style("html,body {width: 100%, height: 100%}") :: + Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text) :: + HTML.style_file(HTTP.CSS_Service.name) :: css ::: js) + } + def build_html( output_file: Path, web_dir: Path = default_web_dir, + web_assets: String = default_web_assets, 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 = - Elm.Project("Find_Facts", web_dir, head = - List( - HTML.style("html,body {width: 100%, height: 100%}"), - Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text), - HTML.style_file(HTTP.CSS_Service.name), - HTML.style_file("https://fonts.googleapis.com/css?family=Roboto:300,400,500|Material+Icons"), - HTML.style_file( - "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(output_file, progress = progress) + Isabelle_System.copy_dir(web_sources_dir, web_dir, direct = true) + web_project(web_dir, web_assets).build_html(output_file, progress = progress) + } + + object Asset { + def parse(s: String): (String, String) = + space_explode(':', s) match { + case file :: mime_type :: Nil => file -> mime_type + case _ => error("Malformed asset: " + quote(s)) + } + + def load(s: String): Asset = { + val (file, mime_type) = parse(s) + val path = web_assets_dir + Path.explode(file) + Asset(path, Bytes.read(path), mime_type) + } + } + + case class Asset(path: Path, content: Bytes, mime_type: String) + + def load_web_assets: List[Asset] = { + val assets = proper_string(default_web_assets) getOrElse error("No find_facts web assets found") + space_explode(',', assets).map(Asset.load) } @@ -928,7 +958,11 @@ File.read(default_web_dir + web_html) } - val html = rebuild() + val digest = web_project(web_sources_dir).sources_shasum.digest + val html = + if (digest != Elm.Project.get_digest(web_assets_dir + web_html)) rebuild() + else File.read(web_assets_dir + web_html) + val web_assets = load_web_assets val solr = Solr.init(solr_data_dir) resolve_indexes(solr) @@ -944,7 +978,13 @@ HTTP.CSS_Service, new HTTP.Service("find_facts") { def apply(request: HTTP.Request): Option[HTTP.Response] = - Some(HTTP.Response.html(if (devel) rebuild() else html)) + if (request.toplevel) Some(HTTP.Response.html(if (devel) rebuild() else html)) + else { + request.uri_path.flatMap(path => web_assets.collectFirst({ + case asset if path == asset.path.base => + HTTP.Response(asset.content, asset.mime_type) + })) + } }, new HTTP.REST_Service("api/block", progress = progress) { def handle(body: JSON.T): Option[JSON.T] =