css service, e.g. for dynamic web apps;
--- 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))