--- a/Admin/components/components.sha1 Sat Feb 08 11:18:30 2025 +0100
+++ b/Admin/components/components.sha1 Sat Feb 08 17:44:04 2025 +0100
@@ -112,6 +112,7 @@
8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
+a7dffe7ab28c0627ef5957ef521ded2db9022b37 find_facts_web-20250208.tar.gz
7a4b46752aa60c1ee6c53a2c128dedc8255a4568 flatlaf-0.46-1.tar.gz
ed5cbc216389b655dac21a19e770a02a96867b85 flatlaf-0.46.tar.gz
d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz
--- a/Admin/components/main Sat Feb 08 11:18:30 2025 +0100
+++ b/Admin/components/main Sat Feb 08 17:44:04 2025 +0100
@@ -8,6 +8,7 @@
elm-0.19.1
easychair-3.5
eptcs-1.7.0
+find_facts_web-20250208
flatlaf-3.5.4-1
foiltex-2.1.4b
idea-icons-20210508
--- a/etc/build.props Sat Feb 08 11:18:30 2025 +0100
+++ b/etc/build.props Sat Feb 08 17:44:04 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 Sat Feb 08 17:44:04 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/General/http.scala Sat Feb 08 11:18:30 2025 +0100
+++ b/src/Pure/General/http.scala Sat Feb 08 17:44:04 2025 +0100
@@ -22,6 +22,8 @@
val mime_type_bytes: String = "application/octet-stream"
val mime_type_text: String = "text/plain; charset=utf-8"
val mime_type_html: String = "text/html; charset=utf-8"
+ val mime_type_css: String = "text/css; charset=utf-8"
+ val mime_type_js: String = "text/javascript; charset=utf-8"
val default_mime_type: String = mime_type_bytes
val default_encoding: String = UTF8.charset.name
@@ -336,7 +338,7 @@
/** Isabelle services **/
def isabelle_services: List[Service] =
- List(Welcome_Service, Fonts_Service, PDFjs_Service, Docs_Service)
+ List(Welcome_Service, Fonts_Service, CSS_Service, PDFjs_Service, Docs_Service)
/* welcome */
@@ -373,6 +375,19 @@
}
+ /* css */
+
+ object CSS_Service extends CSS()
+
+ class CSS(name: String = "css", fonts: String = Fonts_Service.name) extends Service(name) {
+ private lazy val css =
+ HTML.fonts_css("/" + fonts + "/" + _) + "\n\n" + File.read(HTML.isabelle_css)
+
+ def apply(request: Request): Option[Response] =
+ Some(Response(Bytes(css), Content.mime_type_css))
+ }
+
+
/* pdfjs */
object PDFjs_Service extends PDFjs()
--- a/src/Pure/System/isabelle_tool.scala Sat Feb 08 11:18:30 2025 +0100
+++ b/src/Pure/System/isabelle_tool.scala Sat Feb 08 17:44:04 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/elm.scala Sat Feb 08 11:18:30 2025 +0100
+++ b/src/Tools/Find_Facts/src/elm.scala Sat Feb 08 17:44:04 2025 +0100
@@ -18,22 +18,36 @@
object Elm {
+ def elm_home: Path = {
+ Path.explode(proper_string(Isabelle_System.getenv("ISABELLE_ELM_HOME"))
+ getOrElse error("No elm component found"))
+ }
+
object Project {
def apply(
name: String,
dir: Path,
main: Path = Path.explode("src/Main.elm"),
- output: Path = Path.explode("index.html"),
head: XML.Body = Nil
): Project = {
if (!dir.is_dir) error("Project directory does not exist: " + dir)
val main_file = dir + main
if (!main_file.is_file) error("Main elm file does not exist: " + main_file)
- new Project(name, dir, main, dir + output, head)
+ 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, output: Path, head: XML.Body) {
+ class Project private(name: String, dir: Path, main: Path, head: XML.Body) {
val definition = JSON.parse(File.read(dir + Path.basic("elm.json")))
val src_dirs =
JSON.strings(definition, "source-directories").getOrElse(
@@ -54,25 +68,14 @@
meta_info ::: head_digest ::: source_digest
}
- def get_digest: SHA1.Digest =
- Exn.capture {
- val html = HTML.parse_document(File.read(output))
- 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(progress: Progress = new Progress): String = {
+ def build_html(output_file: Path, progress: Progress = new Progress): Unit = {
val digest = sources_shasum.digest
- if (digest == get_digest) File.read(output)
- else {
- progress.echo("Building web application " + output.absolute + " ...")
+ if (digest != Project.get_digest(output_file)) {
+ progress.echo("Building web application " + output_file.absolute + " ...")
val cmd =
- File.bash_path(Path.explode("$ISABELLE_ELM_HOME/elm")) + " make " +
- File.bash_path(main) + " --optimize --output=" + output
+ File.bash_path(elm_home + Path.basic("elm")) + " make " +
+ File.bash_path(main) + " --optimize --output=" + output_file
val res = Isabelle_System.bash(cmd, cwd = dir)
if (!res.ok) {
@@ -80,14 +83,12 @@
error("Failed to compile Elm sources")
}
- val file = HTML.parse_document(File.read(output))
+ val file = HTML.parse_document(File.read(output_file))
file.head.appendChild(
Element("meta").attr("name", "shasum").attr("content", digest.toString))
file.head.append(XML.string_of_body(head))
val html = file.html
- File.write(output, html)
-
- html
+ File.write(output_file, html)
}
}
}
--- a/src/Tools/Find_Facts/src/find_facts.scala Sat Feb 08 11:18:30 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala Sat Feb 08 17:44:04 2025 +0100
@@ -883,10 +883,66 @@
}
- /* find facts */
+ /* web */
+
+ val web_html: Path = Path.basic("index").html
+
+ 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)
+ }
- val web_sources: Path = Path.explode("$FIND_FACTS_HOME/web")
- val web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web")
+ 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_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)
+ }
+
+
+ /* find facts */
def find_facts_server(
options: Options,
@@ -894,25 +950,19 @@
devel: Boolean = false,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.copy_dir(web_sources, web_dir, direct = true)
-
val database = options.string("find_facts_database_name")
val encode = new Encode(options)
- val logo = Bytes.read(web_dir + Path.explode("favicon.ico"))
- val isabelle_style = HTML.fonts_css("/fonts/" + _) + "\n\n" + File.read(HTML.isabelle_css)
+ def rebuild(): String = {
+ build_html(default_web_dir + web_html, progress = progress)
+ File.read(default_web_dir + web_html)
+ }
- 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("isabelle.css"),
- 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")))
-
- val frontend = project.build_html(progress = progress)
+ 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)
@@ -925,14 +975,16 @@
val server =
HTTP.server(port, name = "", services = List(
HTTP.Fonts_Service,
- new HTTP.Service("isabelle.css") {
- def apply(request: HTTP.Request): Option[HTTP.Response] =
- Some(HTTP.Response(Bytes(isabelle_style), "text/css"))
- },
+ HTTP.CSS_Service,
new HTTP.Service("find_facts") {
def apply(request: HTTP.Request): Option[HTTP.Response] =
- Some(HTTP.Response.html(
- if (devel) project.build_html(progress = progress) else frontend))
+ 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] =
--- a/src/Tools/Find_Facts/web/src/Searcher.elm Sat Feb 08 11:18:30 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Searcher.elm Sat Feb 08 17:44:04 2025 +0100
@@ -12,7 +12,7 @@
import Browser.Events as Events
import Dict exposing (Dict)
import Html exposing (..)
-import Html.Attributes exposing (name, style)
+import Html.Attributes exposing (class, name, style)
import Html.Events.Extra exposing (onEnter)
import Html.Extra as Html
import Json.Decode as Decode
@@ -268,6 +268,20 @@
x::xs -> ItemList.list (ItemList.config |> ItemList.setAttributes menu_config) x xs
_ -> Html.nothing
+isabelle_icon_button s =
+ IconButton.customIcon
+ Html.i
+ [class "material-icons", style "vertical-align" "top",
+ style "font-family" "\"Isabelle DejaVu Sans Mono\", monospace", style "font-size" "math"]
+ [Html.text s]
+
+isabelle_icon_textfield s =
+ TextFieldIcon.customIcon
+ Html.i
+ [class "material-icons", style "font-family" "\"Isabelle DejaVu Sans Mono\", monospace",
+ style "font-size" "larger"]
+ [Html.text s]
+
view_filter: Maybe String -> Dict String Int -> (Int, Filter) -> Html Msg
view_filter search0 counts (i, filter) =
let
@@ -281,7 +295,7 @@
[TextField.outlined
(TextField.config
|> TextField.setLeadingIcon (Just (
- TextFieldIcon.icon (if filter.exclude then "block" else "done")
+ isabelle_icon_textfield (if filter.exclude then "∉" else "∈")
|> TextFieldIcon.setOnInteraction (Change_Filter i)))
|> TextField.setValue (Just value)
|> TextField.setOnInput (Input_Filter (Maybe.isNothing search))
@@ -292,7 +306,7 @@
LayoutGrid.cell [LayoutGrid.span1, LayoutGrid.alignLeft] [
IconButton.iconButton
(IconButton.config |> IconButton.setOnClick (Remove_Filter i))
- (IconButton.icon "close")]]
+ (isabelle_icon_button "×")]]
view_facet: String -> String -> List String -> Dict String Int -> Set String -> Html Msg
view_facet field t ts counts selected =