--- 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)
})