# HG changeset patch # User Fabian Huch # Date 1739033044 -3600 # Node ID bb6a3b379f6a23875cb85f48bc4a7cc4339f86ac # Parent 1126ee407227beda2d91bc884a7f107794759e20# Parent eebb8270b3cc1ca36d71b54dac7813e711d9d98c merged diff -r eebb8270b3cc -r bb6a3b379f6a Admin/components/components.sha1 --- 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 diff -r eebb8270b3cc -r bb6a3b379f6a Admin/components/main --- 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 diff -r eebb8270b3cc -r bb6a3b379f6a etc/build.props --- 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 \ diff -r eebb8270b3cc -r bb6a3b379f6a 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 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 diff -r eebb8270b3cc -r bb6a3b379f6a src/Pure/General/http.scala --- 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() diff -r eebb8270b3cc -r bb6a3b379f6a src/Pure/System/isabelle_tool.scala --- 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, diff -r eebb8270b3cc -r bb6a3b379f6a src/Tools/Find_Facts/src/elm.scala --- 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) } } } diff -r eebb8270b3cc -r bb6a3b379f6a src/Tools/Find_Facts/src/find_facts.scala --- 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] = diff -r eebb8270b3cc -r bb6a3b379f6a src/Tools/Find_Facts/web/src/Searcher.elm --- 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 =