--- a/src/Pure/Thy/browser_info.scala Sun Aug 21 12:23:17 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala Sun Aug 21 12:35:45 2022 +0200
@@ -98,6 +98,9 @@
else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
}
+
+ /* preview PIDE document */
+
val isabelle_css: String = File.read(HTML.isabelle_css)
def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document = {
@@ -109,6 +112,31 @@
List(HTML.source(body)), css = "", structural = false)
HTML_Document(title, content)
}
+
+ def preview_document(
+ snapshot: Document.Snapshot,
+ plain_text: Boolean = false,
+ fonts_css: String = HTML.fonts_css()
+ ): HTML_Document = {
+ require(!snapshot.is_outdated, "document snapshot outdated")
+
+ val name = snapshot.node_name
+ if (plain_text) {
+ val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
+ val body = HTML.text(snapshot.node.source)
+ html_document(title, body, fonts_css)
+ }
+ else {
+ Resources.html_document(snapshot) getOrElse {
+ 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 = Node_Context.empty.make_html(elements, xml)
+ html_document(title, body, fonts_css)
+ }
+ }
+ }
}
sealed case class HTML_Document(title: String, content: String)
@@ -307,35 +335,6 @@
}
- /* PIDE HTML document */
-
- def html_document(
- snapshot: Document.Snapshot,
- context: Context,
- plain_text: Boolean = false,
- fonts_css: String = HTML.fonts_css()
- ): HTML_Document = {
- require(!snapshot.is_outdated, "document snapshot outdated")
-
- val name = snapshot.node_name
- if (plain_text) {
- val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
- val body = HTML.text(snapshot.node.source)
- context.html_document(title, body, fonts_css)
- }
- else {
- Resources.html_document(snapshot) getOrElse {
- 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 = context.elements.html)
- val body = Node_Context.empty.make_html(context.elements, xml)
- context.html_document(title, body, fonts_css)
- }
- }
- }
-
-
/** HTML presentation **/
--- a/src/Tools/VSCode/src/preview_panel.scala Sun Aug 21 12:23:17 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala Sun Aug 21 12:35:45 2022 +0200
@@ -28,9 +28,9 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val context =
- Browser_Info.context(resources.sessions_structure, Browser_Info.elements2)
- val document = Browser_Info.html_document(snapshot, context)
+ val document =
+ Browser_Info.context(resources.sessions_structure, Browser_Info.elements2).
+ preview_document(snapshot)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
--- a/src/Tools/jEdit/src/document_model.scala Sun Aug 21 12:23:17 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sun Aug 21 12:35:45 2022 +0200
@@ -313,10 +313,9 @@
}
yield {
val snapshot = model.await_stable_snapshot()
- val context =
- Browser_Info.context(PIDE.resources.sessions_structure, Browser_Info.elements2)
val document =
- Browser_Info.html_document(snapshot, context,
+ Browser_Info.context(PIDE.resources.sessions_structure, Browser_Info.elements2).
+ 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)