# HG changeset patch # User wenzelm # Date 1608387241 -3600 # Node ID 75fc90edc0a86414c18b8ef8ab92b0c1eb5dfb09 # Parent c007d0fa0938a8975dc7e6c30997edc374ba12ce clarified signature and module structure; diff -r c007d0fa0938 -r 75fc90edc0a8 src/Pure/PIDE/resources.scala --- 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 */ diff -r c007d0fa0938 -r 75fc90edc0a8 src/Pure/Thy/bibtex.scala --- 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 } diff -r c007d0fa0938 -r 75fc90edc0a8 src/Pure/Thy/file_format.scala --- 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 */ diff -r c007d0fa0938 -r 75fc90edc0a8 src/Pure/Thy/presentation.scala --- 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") diff -r c007d0fa0938 -r 75fc90edc0a8 src/Tools/VSCode/src/preview_panel.scala --- 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 diff -r c007d0fa0938 -r 75fc90edc0a8 src/Tools/jEdit/src/document_model.scala --- 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) } }