--- a/src/Pure/Thy/presentation.scala Sun Jan 03 12:11:56 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Sun Jan 03 16:21:59 2021 +0100
@@ -56,6 +56,13 @@
/* HTML body */
+ val html_elements1: Markup.Elements =
+ Rendering.foreground_elements ++ Rendering.text_color_elements +
+ Markup.NUMERAL + Markup.COMMENT
+
+ val html_elements2: Markup.Elements =
+ html_elements1 ++ Rendering.markdown_elements + Markup.LANGUAGE
+
private val div_elements =
Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
HTML.descr.name)
@@ -100,14 +107,11 @@
/* PIDE HTML document */
- val html_elements: Markup.Elements =
- Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
- Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
-
def html_document(
resources: Resources,
snapshot: Document.Snapshot,
html_context: HTML_Context,
+ html_elements: Markup.Elements,
plain_text: Boolean = false): HTML_Document =
{
require(!snapshot.is_outdated)
@@ -377,6 +381,7 @@
progress: Progress = new Progress,
verbose: Boolean = false,
html_context: HTML_Context,
+ html_elements: Markup.Elements,
presentation: Context)
{
val info = deps.sessions_structure(session)
--- a/src/Pure/Tools/build.scala Sun Jan 03 12:11:56 2021 +0100
+++ b/src/Pure/Tools/build.scala Sun Jan 03 16:21:59 2021 +0100
@@ -515,7 +515,8 @@
progress.echo("Presenting " + session_name + " ...")
Presentation.session_html(
resources, session_name, deps, db_context, progress = progress,
- verbose = verbose, html_context = html_context, presentation = presentation)
+ verbose = verbose, html_context = html_context,
+ html_elements = Presentation.html_elements1, presentation = presentation)
})
val browser_chapters =
--- a/src/Tools/VSCode/src/preview_panel.scala Sun Jan 03 12:11:56 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Sun Jan 03 16:21:59 2021 +0100
@@ -31,7 +31,9 @@
if (snapshot.is_outdated) m
else {
val html_context = Presentation.html_context()
- val document = Presentation.html_document(resources, snapshot, html_context)
+ val document =
+ Presentation.html_document(
+ resources, snapshot, html_context, Presentation.html_elements2)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
--- a/src/Tools/jEdit/src/document_model.scala Sun Jan 03 12:11:56 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Jan 03 16:21:59 2021 +0100
@@ -321,7 +321,8 @@
val snapshot = model.await_stable_snapshot()
val html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
val document =
- Presentation.html_document(PIDE.resources, snapshot, html_context,
+ Presentation.html_document(
+ PIDE.resources, snapshot, html_context, Presentation.html_elements2,
plain_text = query.startsWith(plain_text_prefix))
HTTP.Response.html(document.content)
})