# HG changeset patch # User Fabian Huch # Date 1738765697 -3600 # Node ID 6c3b7d1f2115458fb0e51c1fba55674590f1373b # Parent 27acc91b3fbfde89ed17c6752e18e1e0e361dc03 css service, e.g. for dynamic web apps; diff -r 27acc91b3fbf -r 6c3b7d1f2115 src/Pure/General/http.scala --- a/src/Pure/General/http.scala Wed Feb 05 15:05:10 2025 +0100 +++ b/src/Pure/General/http.scala Wed Feb 05 15:28:17 2025 +0100 @@ -338,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 */ @@ -375,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 27acc91b3fbf -r 6c3b7d1f2115 src/Tools/Find_Facts/src/find_facts.scala --- a/src/Tools/Find_Facts/src/find_facts.scala Wed Feb 05 15:05:10 2025 +0100 +++ b/src/Tools/Find_Facts/src/find_facts.scala Wed Feb 05 15:28:17 2025 +0100 @@ -896,7 +896,7 @@ 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(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"), @@ -917,8 +917,6 @@ val database = options.string("find_facts_database_name") val encode = new Encode(options) - val isabelle_style = HTML.fonts_css("/fonts/" + _) + "\n\n" + File.read(HTML.isabelle_css) - val html = build_html(progress = progress) val solr = Solr.init(solr_data_dir) @@ -932,10 +930,7 @@ 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) build_html(progress = progress) else html))