--- a/src/Pure/PIDE/resources.scala Sat Dec 19 12:05:17 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Dec 19 15:14:01 2020 +0100
@@ -57,8 +57,8 @@
def is_hidden(name: Document.Node.Name): Boolean =
!name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
- def file_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
- File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
+ def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
+ File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
/* file-system operations */
--- a/src/Pure/Thy/bibtex.scala Sat Dec 19 12:05:17 2020 +0100
+++ b/src/Pure/Thy/bibtex.scala Sat Dec 19 15:14:01 2020 +0100
@@ -30,7 +30,7 @@
"""theory "bib" imports Pure begin bibtex_file """ +
Outer_Syntax.quote_string(name) + """ end"""
- override def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
+ override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
{
val name = snapshot.node_name
if (detect(name.node)) {
@@ -40,7 +40,7 @@
File.write(bib, snapshot.node.source)
Bibtex.html_output(List(bib), style = "unsort", title = title)
}
- Some(Presentation.Preview(title, content))
+ Some(Presentation.HTML_Document(title, content))
}
else None
}
--- a/src/Pure/Thy/file_format.scala Sat Dec 19 12:05:17 2020 +0100
+++ b/src/Pure/Thy/file_format.scala Sat Dec 19 15:14:01 2020 +0100
@@ -89,7 +89,7 @@
} yield s
}
- def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = None
+ def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = None
/* PIDE session agent */
--- a/src/Pure/Thy/presentation.scala Sat Dec 19 12:05:17 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Sat Dec 19 15:14:01 2020 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/present.scala
Author: Makarius
-Theory presentation: HTML and LaTeX documents.
+HTML/PDF presentation of theory documents.
*/
package isabelle
@@ -12,6 +12,100 @@
object Presentation
{
+ /** HTML documents **/
+
+ sealed case class HTML_Document(title: String, content: String)
+
+
+ /* HTML body */
+
+ private val div_elements =
+ Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
+ HTML.descr.name)
+
+ private def html_div(html: XML.Body): Boolean =
+ html exists {
+ case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
+ case XML.Text(_) => false
+ }
+
+ private def html_class(c: String, html: XML.Body): XML.Tree =
+ if (html.forall(_ == HTML.no_text)) HTML.no_text
+ else if (html_div(html)) HTML.div(c, html)
+ else HTML.span(c, html)
+
+ private def html_body(xml: XML.Body): XML.Body =
+ xml map {
+ case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
+ html_class(Markup.Language.DOCUMENT, html_body(body))
+ case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body))
+ case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body))
+ case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
+ case XML.Elem(Markup.Markdown_List(kind), body) =>
+ if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body))
+ case XML.Elem(markup, body) =>
+ val name = markup.name
+ val html =
+ markup.properties match {
+ case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
+ List(html_class(kind, html_body(body)))
+ case _ =>
+ html_body(body)
+ }
+ Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
+ case Some(c) => html_class(c.toString, html)
+ case None => html_class(name, html)
+ }
+ case XML.Text(text) =>
+ XML.Text(Symbol.decode(text))
+ }
+
+
+ /* PIDE HTML document */
+
+ val html_elements: Markup.Elements =
+ Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
+ Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
+
+ def html_document(
+ resources: Resources,
+ snapshot: Document.Snapshot,
+ plain_text: Boolean = false,
+ fonts_url: String => String = HTML.fonts_url()): HTML_Document =
+ {
+ require(!snapshot.is_outdated)
+
+ def output_document(title: String, body: XML.Body): String =
+ HTML.output_document(
+ List(
+ HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
+ HTML.title(title)),
+ List(HTML.source(body)), css = "", structural = false)
+
+ val name = snapshot.node_name
+
+ if (plain_text) {
+ val title = "File " + quote(name.path.file_name)
+ val content = output_document(title, HTML.text(snapshot.node.source))
+ HTML_Document(title, content)
+ }
+ else {
+ resources.html_document(snapshot) match {
+ case Some(document) => document
+ case None =>
+ val title =
+ if (name.is_theory) "Theory " + quote(name.theory_base_name)
+ else "File " + quote(name.path.file_name)
+ val body = html_body(snapshot.xml_markup(elements = html_elements))
+ HTML_Document(title, output_document(title, body))
+ }
+ }
+ }
+
+
+
+ /** PDF LaTeX documents **/
+
/* document info */
abstract class Document_Name
@@ -152,6 +246,9 @@
}
+
+ /** HTML presentation **/
+
/* maintain chapter index */
private val sessions_path = Path.basic(".sessions")
@@ -349,98 +446,6 @@
- /** preview **/
-
- sealed case class Preview(title: String, content: String)
-
- def preview(
- resources: Resources,
- snapshot: Document.Snapshot,
- plain_text: Boolean = false,
- fonts_url: String => String = HTML.fonts_url()): Preview =
- {
- require(!snapshot.is_outdated)
-
- def output_document(title: String, body: XML.Body): String =
- HTML.output_document(
- List(
- HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
- HTML.title(title)),
- List(HTML.source(body)), css = "", structural = false)
-
- val name = snapshot.node_name
-
- if (plain_text) {
- val title = "File " + quote(name.path.file_name)
- val content = output_document(title, HTML.text(snapshot.node.source))
- Preview(title, content)
- }
- else {
- resources.file_preview(snapshot) match {
- case Some(preview) => preview
- case None =>
- val title =
- if (name.is_theory) "Theory " + quote(name.theory_base_name)
- else "File " + quote(name.path.file_name)
- val content = output_document(title, pide_document(snapshot))
- Preview(title, content)
- }
- }
- }
-
-
- /* PIDE document */
-
- private val document_elements =
- Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
- Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
-
- private val div_elements =
- Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
- HTML.descr.name)
-
- private def html_div(html: XML.Body): Boolean =
- html exists {
- case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
- case XML.Text(_) => false
- }
-
- private def html_class(c: String, html: XML.Body): XML.Tree =
- if (html.forall(_ == HTML.no_text)) HTML.no_text
- else if (html_div(html)) HTML.div(c, html)
- else HTML.span(c, html)
-
- private def make_html(xml: XML.Body): XML.Body =
- xml map {
- case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
- html_class(Markup.Language.DOCUMENT, make_html(body))
- case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body))
- case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body))
- case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
- case XML.Elem(Markup.Markdown_List(kind), body) =>
- if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body))
- case XML.Elem(markup, body) =>
- val name = markup.name
- val html =
- markup.properties match {
- case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
- List(html_class(kind, make_html(body)))
- case _ =>
- make_html(body)
- }
- Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
- case Some(c) => html_class(c.toString, html)
- case None => html_class(name, html)
- }
- case XML.Text(text) =>
- XML.Text(Symbol.decode(text))
- }
-
- def pide_document(snapshot: Document.Snapshot): XML.Body =
- make_html(snapshot.xml_markup(elements = document_elements))
-
-
-
/** build documents **/
val session_tex_path = Path.explode("session.tex")
--- a/src/Tools/VSCode/src/preview_panel.scala Sat Dec 19 12:05:17 2020 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Sat Dec 19 15:14:01 2020 +0100
@@ -30,8 +30,8 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val preview = Presentation.preview(resources, snapshot)
- channel.write(LSP.Preview_Response(file, column, preview.title, preview.content))
+ val document = Presentation.html_document(resources, snapshot)
+ channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
case None => m - file
--- a/src/Tools/jEdit/src/document_model.scala Sat Dec 19 12:05:17 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sat Dec 19 15:14:01 2020 +0100
@@ -310,7 +310,7 @@
val fonts_root = http_root + "/fonts"
val preview_root = http_root + "/preview"
- val preview =
+ val html =
HTTP.get(preview_root, arg =>
for {
query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
@@ -319,13 +319,14 @@
}
yield {
val snapshot = model.await_stable_snapshot()
- val preview =
- Presentation.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
+ val document =
+ Presentation.html_document(PIDE.resources, snapshot,
+ fonts_url = HTML.fonts_dir(fonts_root),
plain_text = query.startsWith(plain_text_prefix))
- HTTP.Response.html(preview.content)
+ HTTP.Response.html(document.content)
})
- List(HTTP.fonts(fonts_root), preview)
+ List(HTTP.fonts(fonts_root), html)
}
}