# HG changeset patch
# User wenzelm
# Date 1672430990 -3600
# Node ID 5ab016cbba18ace38a173e25138e759bcf9ec63b
# Parent  f2a8ba0b8c96bfdf36074ac150560505d138fae7
proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;

diff -r f2a8ba0b8c96 -r 5ab016cbba18 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)
       }
+    }
   }
 }