css service, e.g. for dynamic web apps;
authorFabian Huch <huch@in.tum.de>
Wed, 05 Feb 2025 15:28:17 +0100
changeset 82107 6c3b7d1f2115
parent 82106 27acc91b3fbf
child 82108 a4947e9bbf62
css service, e.g. for dynamic web apps;
src/Pure/General/http.scala
src/Tools/Find_Facts/src/find_facts.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()
--- 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))