proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 30 20:38:29 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Dec 30 21:09:50 2022 +0100
@@ -314,7 +314,7 @@
PIDE.plugin.http_server.url + "/" + service.name + "?" +
(if (plain_text) plain_text_prefix else "") + Url.encode(node_name.node)
- def apply(request: HTTP.Request): Option[HTTP.Response] =
+ def apply(request: HTTP.Request): Option[HTTP.Response] = GUI_Thread.now {
for {
query <- request.decode_query
name = Library.perhaps_unprefix(plain_text_prefix, query)
@@ -331,6 +331,7 @@
fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
HTTP.Response.html(document.content)
}
+ }
}
}