src/Tools/jEdit/src/document_model.scala
changeset 72959 a093b8fc9e21
parent 72957 75fc90edc0a8
child 72960 f7fc8e7c50b0
--- a/src/Tools/jEdit/src/document_model.scala	Sat Dec 19 15:32:29 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Dec 20 12:24:41 2020 +0100
@@ -319,9 +319,9 @@
         }
         yield {
           val snapshot = model.await_stable_snapshot()
+          val context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
           val document =
-            Presentation.html_document(PIDE.resources, snapshot,
-              fonts_url = HTML.fonts_dir(fonts_root),
+            Presentation.html_document(PIDE.resources, snapshot, context,
               plain_text = query.startsWith(plain_text_prefix))
           HTTP.Response.html(document.content)
         })