# HG changeset patch
# User wenzelm
# Date 1609687319 -3600
# Node ID b028e8d22d8df3e09daf3816705cff6207055622
# Parent  03e78b35ebbc2da87efd823db32a590236261815
clarified HTML presentation elements;

diff -r 03e78b35ebbc -r b028e8d22d8d src/Pure/Thy/presentation.scala
--- 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)
diff -r 03e78b35ebbc -r b028e8d22d8d src/Pure/Tools/build.scala
--- 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 =
diff -r 03e78b35ebbc -r b028e8d22d8d src/Tools/VSCode/src/preview_panel.scala
--- 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
               }
diff -r 03e78b35ebbc -r b028e8d22d8d src/Tools/jEdit/src/document_model.scala
--- 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)
         })