tuned;
authorwenzelm
Sun, 20 Dec 2020 13:20:09 +0100
changeset 72961 f78730341c87
parent 72960 f7fc8e7c50b0
child 72962 af2d0e07493b
tuned;
src/Tools/VSCode/src/preview_panel.scala
src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/VSCode/src/preview_panel.scala	Sun Dec 20 12:32:12 2020 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Sun Dec 20 13:20:09 2020 +0100
@@ -30,8 +30,8 @@
               val snapshot = model.snapshot()
               if (snapshot.is_outdated) m
               else {
-                val context = Presentation.html_context()
-                val document = Presentation.html_document(resources, snapshot, context)
+                val html_context = Presentation.html_context()
+                val document = Presentation.html_document(resources, snapshot, html_context)
                 channel.write(LSP.Preview_Response(file, column, document.title, document.content))
                 m - file
               }
--- a/src/Tools/jEdit/src/document_model.scala	Sun Dec 20 12:32:12 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Dec 20 13:20:09 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 html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
           val document =
-            Presentation.html_document(PIDE.resources, snapshot, context,
+            Presentation.html_document(PIDE.resources, snapshot, html_context,
               plain_text = query.startsWith(plain_text_prefix))
           HTTP.Response.html(document.content)
         })