--- 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()
--- 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))
}
--- 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
}
--- 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)
})
--- 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)