--- a/src/Pure/Thy/presentation.scala Tue Jan 05 13:08:45 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Tue Jan 05 14:21:18 2021 +0100
@@ -54,20 +54,31 @@
}
- /* HTML body */
+ /* presentation elements */
+
+ sealed case class Elements(
+ html: Markup.Elements = Markup.Elements.empty,
+ language: Markup.Elements = Markup.Elements.empty)
- val html_elements1: Markup.Elements =
- Rendering.foreground_elements ++ Rendering.text_color_elements +
- Markup.NUMERAL + Markup.COMMENT
+ val elements1: Elements =
+ Elements(
+ html =
+ Rendering.foreground_elements ++ Rendering.text_color_elements +
+ Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE)
- val html_elements2: Markup.Elements =
- html_elements1 ++ Rendering.markdown_elements + Markup.LANGUAGE
+ val elements2: Elements =
+ Elements(
+ html = elements1.html ++ Rendering.markdown_elements,
+ language = elements1.language + Markup.Language.DOCUMENT)
+
+
+ /* HTML */
private val div_elements =
Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
HTML.descr.name)
- def make_html_body(xml: XML.Body): XML.Body =
+ def make_html(elements: Elements, xml: XML.Body): XML.Body =
{
def html_div(html: XML.Body): Boolean =
html exists {
@@ -75,26 +86,29 @@
case XML.Text(_) => false
}
- def html_class(c: String, html: XML.Body): XML.Tree =
- if (html.forall(_ == XML.no_text)) XML.no_text
- else if (html_div(html)) HTML.div(c, html)
- else HTML.span(c, html)
+ def html_class(c: String, html: XML.Body): XML.Body =
+ if (c == "") html
+ else if (html_div(html)) List(HTML.div(c, html))
+ else List(HTML.span(c, html))
def html_body(xml_body: XML.Body): XML.Body =
- xml_body map {
- case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
- html_class(Markup.Language.DOCUMENT, html_body(body))
- case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body))
- case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body))
- case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text
+ xml_body flatMap {
+ case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
+ html_class(if (elements.language(name)) name else "", html_body(body))
+ case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) =>
+ List(HTML.par(html_body(body)))
+ case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) =>
+ List(HTML.item(html_body(body)))
+ case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => Nil
case XML.Elem(Markup.Markdown_List(kind), body) =>
- if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body))
+ if (kind == Markup.ENUMERATE) List(HTML.enum(html_body(body)))
+ else List(HTML.list(html_body(body)))
case XML.Elem(markup, body) =>
val name = markup.name
val html =
markup.properties match {
case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
- List(html_class(kind, html_body(body)))
+ html_class(kind, html_body(body))
case _ =>
html_body(body)
}
@@ -103,7 +117,7 @@
case None => html_class(name, html)
}
case XML.Text(text) =>
- XML.Text(Symbol.decode(text))
+ HTML.text(Symbol.decode(text))
}
html_body(xml)
@@ -116,7 +130,7 @@
resources: Resources,
snapshot: Document.Snapshot,
html_context: HTML_Context,
- html_elements: Markup.Elements,
+ elements: Elements,
plain_text: Boolean = false): HTML_Document =
{
require(!snapshot.is_outdated)
@@ -132,7 +146,7 @@
val title =
if (name.is_theory) "Theory " + quote(name.theory_base_name)
else "File " + Symbol.cartouche_decoded(name.path.file_name)
- val body = make_html_body(snapshot.xml_markup(elements = html_elements))
+ val body = make_html(elements, snapshot.xml_markup(elements = elements.html))
html_context.html_document(title, body)
}
}
@@ -395,7 +409,7 @@
progress: Progress = new Progress,
verbose: Boolean = false,
html_context: HTML_Context,
- html_elements: Markup.Elements,
+ elements: Elements,
presentation: Context)
{
val info = deps.sessions_structure(session)
@@ -482,7 +496,7 @@
val files =
for {
- (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements)
+ (src_path, xml) <- snapshot.xml_markup_blobs(elements = elements.html)
if xml.nonEmpty
}
yield {
@@ -504,7 +518,7 @@
val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
HTML.write_document(file_path.dir, file_path.file_name,
List(HTML.title(file_title)),
- List(html_context.head(file_title), html_context.source(make_html_body(xml))))
+ List(html_context.head(file_title), html_context.source(make_html(elements, xml))))
List(HTML.link(file_name, HTML.text(file_title)))
}
--- a/src/Pure/Tools/build.scala Tue Jan 05 13:08:45 2021 +0100
+++ b/src/Pure/Tools/build.scala Tue Jan 05 14:21:18 2021 +0100
@@ -516,7 +516,7 @@
Presentation.session_html(
resources, session_name, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
- html_elements = Presentation.html_elements1, presentation = presentation)
+ elements = Presentation.elements1, presentation = presentation)
})
val browser_chapters =
--- a/src/Tools/VSCode/src/preview_panel.scala Tue Jan 05 13:08:45 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Tue Jan 05 14:21:18 2021 +0100
@@ -33,7 +33,7 @@
val html_context = Presentation.html_context()
val document =
Presentation.html_document(
- resources, snapshot, html_context, Presentation.html_elements2)
+ resources, snapshot, html_context, Presentation.elements2)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Jan 05 13:08:45 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Jan 05 14:21:18 2021 +0100
@@ -322,7 +322,7 @@
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_elements2,
+ PIDE.resources, snapshot, html_context, Presentation.elements2,
plain_text = query.startsWith(plain_text_prefix))
HTTP.Response.html(document.content)
})