--- 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 \
--- /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
--- 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,
--- 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] =