--- a/src/Pure/Thy/presentation.scala Thu Aug 18 11:24:20 2022 +0200
+++ b/src/Pure/Thy/presentation.scala Thu Aug 18 11:43:27 2022 +0200
@@ -19,12 +19,14 @@
def html_context(
sessions_structure: Sessions.Structure,
+ elements: Elements,
root_dir: Path = Path.current,
nodes: Nodes = Nodes.empty
- ): HTML_Context = new HTML_Context(sessions_structure, root_dir, nodes)
+ ): HTML_Context = new HTML_Context(sessions_structure, elements, root_dir, nodes)
class HTML_Context private[Presentation](
sessions_structure: Sessions.Structure,
+ val elements: Elements,
val root_dir: Path,
val nodes: Nodes
) {
@@ -33,6 +35,9 @@
def theory_session(name: Document.Node.Name): String =
sessions_structure.theory_qualifier(name)
+ def theory_elements(name: Document.Node.Name): Elements =
+ elements.copy(entity = nodes(name.theory).others.foldLeft(elements.entity)(_ + _))
+
def session_dir(name: String): Path =
root_dir + Path.explode(sessions_structure(name).chapter_session)
@@ -379,7 +384,6 @@
def html_document(
snapshot: Document.Snapshot,
html_context: HTML_Context,
- elements: Elements,
plain_text: Boolean = false,
fonts_css: String = HTML.fonts_css()
): HTML_Document = {
@@ -396,8 +400,8 @@
val title =
if (name.is_theory) "Theory " + quote(name.theory_base_name)
else "File " + Symbol.cartouche_decoded(name.path.file_name)
- val xml = snapshot.xml_markup(elements = elements.html)
- val body = make_html(Entity_Context.empty, elements, xml)
+ val xml = snapshot.xml_markup(elements = html_context.elements.html)
+ val body = make_html(Entity_Context.empty, html_context.elements, xml)
html_context.html_document(title, body, fonts_css)
}
}
@@ -529,7 +533,6 @@
def session_html(
html_context: HTML_Context,
session_context: Export.Session_Context,
- session_elements: Elements,
progress: Progress = new Progress,
verbose: Boolean = false,
): Unit = {
@@ -596,9 +599,7 @@
if (verbose) progress.echo("Presenting theory " + name)
val snapshot = Document.State.init.snippet(command)
- val thy_elements =
- session_elements.copy(entity =
- html_context.nodes(name.theory).others.foldLeft(session_elements.entity)(_ + _))
+ val thy_elements = html_context.theory_elements(name)
val files_html =
for {
--- a/src/Pure/Tools/build.scala Thu Aug 18 11:24:20 2022 +0200
+++ b/src/Pure/Tools/build.scala Thu Aug 18 11:43:27 2022 +0200
@@ -504,13 +504,11 @@
progress.echo("Presenting " + session + " ...")
val html_context =
- Presentation.html_context(
- sessions_structure = deps.sessions_structure,
- root_dir = presentation_dir,
- nodes = presentation_nodes)
+ Presentation.html_context(deps.sessions_structure, Presentation.elements1,
+ root_dir = presentation_dir, nodes = presentation_nodes)
using(database_context.open_session(deps.base_info(session))) { session_context =>
- Presentation.session_html(html_context, session_context, Presentation.elements1,
+ Presentation.session_html(html_context, session_context,
progress = progress, verbose = verbose)
}
}, presentation_sessions.map(_.name))
--- a/src/Tools/VSCode/src/preview_panel.scala Thu Aug 18 11:24:20 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala Thu Aug 18 11:43:27 2022 +0200
@@ -28,9 +28,9 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val html_context = Presentation.html_context(resources.sessions_structure)
- val document =
- Presentation.html_document(snapshot, html_context, Presentation.elements2)
+ val html_context =
+ Presentation.html_context(resources.sessions_structure, Presentation.elements2)
+ val document = Presentation.html_document(snapshot, html_context)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
--- a/src/Tools/jEdit/src/document_model.scala Thu Aug 18 11:24:20 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Thu Aug 18 11:43:27 2022 +0200
@@ -313,10 +313,10 @@
}
yield {
val snapshot = model.await_stable_snapshot()
- val html_context = Presentation.html_context(PIDE.resources.sessions_structure)
+ val html_context =
+ Presentation.html_context(PIDE.resources.sessions_structure, Presentation.elements2)
val document =
- Presentation.html_document(
- snapshot, html_context, Presentation.elements2,
+ Presentation.html_document(snapshot, html_context,
plain_text = query.startsWith(plain_text_prefix),
fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
HTTP.Response.html(document.content)