# HG changeset patch
# User wenzelm
# Date 1660815807 -7200
# Node ID 989847d1ebabd9592c69349824bedd1b836dce20
# Parent  25fc7501b8827c46e29a834782952936727d5a8f
clarified signature;

diff -r 25fc7501b882 -r 989847d1ebab src/Pure/Thy/presentation.scala
--- 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 {
diff -r 25fc7501b882 -r 989847d1ebab src/Pure/Tools/build.scala
--- 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))
diff -r 25fc7501b882 -r 989847d1ebab src/Tools/VSCode/src/preview_panel.scala
--- 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
                 }
diff -r 25fc7501b882 -r 989847d1ebab src/Tools/jEdit/src/document_model.scala
--- 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)