# HG changeset patch
# User wenzelm
# Date 1661507825 -7200
# Node ID 29d813c431bbe5510aa75b364d561ec34e6d915a
# Parent  0b4944b25b9da9705f720fa03db97c5d71b25c09
clarified signature;

diff -r 0b4944b25b9d -r 29d813c431bb src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Aug 26 11:46:53 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Fri Aug 26 11:57:05 2022 +0200
@@ -145,16 +145,16 @@
     entity: Markup.Elements = Markup.Elements.empty,
     language: Markup.Elements = Markup.Elements.empty)
 
-  val elements1: Elements =
+  val default_elements: Elements =
     Elements(
       html = Rendering.foreground_elements ++ Rendering.text_color_elements +
         Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
       entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
         Markup.CLASS, Markup.LOCALE, Markup.FREE))
 
-  val elements2: Elements =
+  val extra_elements: Elements =
     Elements(
-      html = elements1.html ++ Rendering.markdown_elements,
+      html = default_elements.html ++ Rendering.markdown_elements,
       language = Markup.Elements(Markup.Language.DOCUMENT))
 
 
@@ -163,7 +163,7 @@
 
   def context(
     sessions_structure: Sessions.Structure,
-    elements: Elements,
+    elements: Elements = default_elements,
     root_dir: Path = Path.current,
     document_info: Document_Info = Document_Info.empty
   ): Context = new Context(sessions_structure, elements, root_dir, document_info)
@@ -647,7 +647,7 @@
     progress.echo("Presentation in " + root_dir)
 
     using(Export.open_database_context(store)) { database_context =>
-      val context0 = context(deps.sessions_structure, elements1, root_dir = root_dir)
+      val context0 = context(deps.sessions_structure, root_dir = root_dir)
 
       val sessions1 =
         deps.sessions_structure.build_requirements(sessions).filter { session_name =>
@@ -662,7 +662,7 @@
         }
 
       val context1 =
-        context(deps.sessions_structure, elements1, root_dir = root_dir,
+        context(deps.sessions_structure, root_dir = root_dir,
           document_info = Document_Info.read(database_context, deps, sessions1))
 
       context1.update_root()
diff -r 0b4944b25b9d -r 29d813c431bb src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Fri Aug 26 11:46:53 2022 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Fri Aug 26 11:57:05 2022 +0200
@@ -46,7 +46,7 @@
                 uri = File.uri(Path.explode(source).absolute_file)
               } yield HTML.link(uri.toString + "#" + def_line, body)
           }
-        val elements = Browser_Info.elements2.copy(entity = Markup.Elements.full)
+        val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
         val html = node_context.make_html(elements, Pretty.separate(st1.output))
         channel.write(LSP.Dynamic_Output(HTML.source(html).toString))
       }
diff -r 0b4944b25b9d -r 29d813c431bb src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala	Fri Aug 26 11:46:53 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Aug 26 11:57:05 2022 +0200
@@ -28,9 +28,10 @@
                 val snapshot = model.snapshot()
                 if (snapshot.is_outdated) m
                 else {
-                  val document =
-                    Browser_Info.context(resources.sessions_structure, Browser_Info.elements2).
-                      preview_document(snapshot)
+                  val context =
+                    Browser_Info.context(resources.sessions_structure,
+                      elements = Browser_Info.extra_elements)
+                  val document = context.preview_document(snapshot)
                   channel.write(LSP.Preview_Response(file, column, document.title, document.content))
                   m - file
                 }
diff -r 0b4944b25b9d -r 29d813c431bb src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Fri Aug 26 11:46:53 2022 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Fri Aug 26 11:57:05 2022 +0200
@@ -69,7 +69,7 @@
                   uri = File.uri(Path.explode(source).absolute_file)
                 } yield HTML.link(uri.toString + "#" + def_line, body)
             }
-          val elements = Browser_Info.elements2.copy(entity = Markup.Elements.full)
+          val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)
           val html = node_context.make_html(elements, Pretty.separate(body))
           output(HTML.source(html).toString)
         })
diff -r 0b4944b25b9d -r 29d813c431bb src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 26 11:46:53 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 26 11:57:05 2022 +0200
@@ -313,9 +313,11 @@
       }
       yield {
         val snapshot = model.await_stable_snapshot()
+        val context =
+          Browser_Info.context(PIDE.resources.sessions_structure,
+            elements = Browser_Info.extra_elements)
         val document =
-          Browser_Info.context(PIDE.resources.sessions_structure, Browser_Info.elements2).
-            preview_document(snapshot,
+          context.preview_document(snapshot,
             plain_text = query.startsWith(plain_text_prefix),
             fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
         HTTP.Response.html(document.content)