proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
authorwenzelm
Fri, 30 Dec 2022 21:09:50 +0100
changeset 76830 5ab016cbba18
parent 76829 f2a8ba0b8c96
child 76831 72daee8a39ca
proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
src/Tools/jEdit/src/document_model.scala
--- 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)
       }
+    }
   }
 }