# HG changeset patch # User wenzelm # Date 1608493783 -3600 # Node ID b7c9d6e4823770d5a09c0f49e28e1a525f383081 # Parent eb1e5c4f70cd6d890f9f5ecd9a8e8bf2f083a4e5# Parent 2621225b4bdd3a108b46d13a2c04d7d7110656b6 merged diff -r eb1e5c4f70cd -r b7c9d6e48237 etc/isabelle.css --- a/etc/isabelle.css Sat Dec 19 17:49:14 2020 +0000 +++ b/etc/isabelle.css Sun Dec 20 20:49:43 2020 +0100 @@ -20,7 +20,7 @@ font-family: "Isabelle DejaVu Sans Mono", monospace; } -.theories { background-color: #FFFFFF; padding: 10px; } +.contents { background-color: #FFFFFF; padding: 10px; } .sessions { background-color: #FFFFFF; padding: 10px; } .document { white-space: normal; font-family: "Isabelle DejaVu Serif", serif; } diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/General/path.scala Sun Dec 20 20:49:43 2020 +0100 @@ -67,6 +67,15 @@ case Parent => ".." } + private def squash_elem(elem: Elem): String = + elem match { + case Root("") => "ROOT" + case Root(s) => "SERVER_" + s + case Basic(s) => s + case Variable(s) => s + case Parent => "PARENT" + } + /* path constructors */ @@ -201,6 +210,7 @@ } def xz: Path = ext("xz") + def html: Path = ext("html") def tex: Path = ext("tex") def pdf: Path = ext("pdf") def thy: Path = ext("thy") @@ -234,6 +244,8 @@ def drop_ext: Path = split_ext._1 def get_ext: String = split_ext._2 + def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem)))) + /* expand */ diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/PIDE/command.scala Sun Dec 20 20:49:43 2020 +0100 @@ -30,7 +30,7 @@ src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) { - def read_file: String = File.read(name.path) + def read_file: Bytes = Bytes.read(name.path) def chunk_file: Symbol.Text_Chunk.File = Symbol.Text_Chunk.File(name.node) diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/PIDE/document.scala Sun Dec 20 20:49:43 2020 +0100 @@ -592,7 +592,7 @@ /* command as add-on snippet */ - def command_snippet(command: Command): Snapshot = + def snippet(command: Command): Snapshot = { val node_name = command.node_name @@ -620,16 +620,23 @@ elements: Markup.Elements = Markup.Elements.full): XML.Body = state.xml_markup(version, node_name, range = range, elements = elements) - def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full): List[XML.Body] = + def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full) + : List[(Path, XML.Body)] = { snippet_command match { case None => Nil case Some(command) => for (Exn.Res(blob) <- command.blobs) yield { - val text = blob.read_file - val markup = command.init_markups(Command.Markup_Index.blob(blob)) - markup.to_XML(Text.Range(0, text.length), text, elements) + val bytes = blob.read_file + val text = bytes.text + val xml = + if (Bytes(text) == bytes) { + val markup = command.init_markups(Command.Markup_Index.blob(blob)) + markup.to_XML(Text.Range(0, text.length), text, elements) + } + else Nil + blob.src_path -> xml } } } @@ -998,8 +1005,7 @@ Command.unparsed(command.source, theory = true, id = id, node_name = node_name, blobs_info = command.blobs_info, results = st.results, markups = st.markups) val state1 = copy(theories = theories - id) - val snapshot = state1.command_snippet(command1) - (snapshot, state1) + (state1.snippet(command1), state1) } def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) @@ -1252,7 +1258,7 @@ new Snapshot(this, version, node_name, edits, snippet_command) } - def command_snippet(command: Command): Snapshot = - snapshot().command_snippet(command) + def snippet(command: Command): Snapshot = + snapshot().snippet(command) } } diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/PIDE/resources.scala Sun Dec 20 20:49:43 2020 +0100 @@ -12,6 +12,12 @@ import java.io.{File => JFile} +object Resources +{ + def empty: Resources = + new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) +} + class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base, @@ -54,12 +60,12 @@ def make_theory_content(thy_name: Document.Node.Name): Option[String] = File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) - def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = - File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot)) - def is_hidden(name: Document.Node.Name): Boolean = !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) + 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 eb1e5c4f70cd -r b7c9d6e48237 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/ROOT.ML Sun Dec 20 20:49:43 2020 +0100 @@ -354,4 +354,3 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" - diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/Thy/bibtex.scala Sun Dec 20 20:49:43 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 eb1e5c4f70cd -r b7c9d6e48237 src/Pure/Thy/file_format.scala --- a/src/Pure/Thy/file_format.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/Thy/file_format.scala Sun Dec 20 20:49:43 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 eb1e5c4f70cd -r b7c9d6e48237 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/Thy/presentation.scala Sun Dec 20 20:49:43 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,127 @@ object Presentation { + /** HTML documents **/ + + val fonts_path = Path.explode("fonts") + + sealed case class HTML_Document(title: String, content: String) + + def html_context(fonts_url: String => String = HTML.fonts_url()): HTML_Context = + new HTML_Context(fonts_url) + + final class HTML_Context private[Presentation](fonts_url: String => String) + { + def init_fonts(dir: Path) + { + val fonts_dir = Isabelle_System.make_directory(dir + fonts_path) + for (entry <- Isabelle_Fonts.fonts(hidden = true)) + File.copy(entry.path, fonts_dir) + } + + def head(title: String, rest: XML.Body = Nil): XML.Tree = + HTML.div("head", HTML.chapter(title) :: rest) + + def source(body: XML.Body): XML.Tree = HTML.pre("source", body) + + def contents(heading: String, items: List[XML.Body], css_class: String = "contents") + : List[XML.Elem] = + { + if (items.isEmpty) Nil + else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items)))) + } + + 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) + + def html_document(title: String, body: XML.Body): HTML_Document = + HTML_Document(title, output_document(title, body)) + } + + + /* 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, + html_context: HTML_Context, + plain_text: Boolean = false): HTML_Document = + { + require(!snapshot.is_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_context.html_document(title, body) + } + 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 body = html_body(snapshot.xml_markup(elements = html_elements)) + html_context.html_document(title, body) + } + } + } + + + + /** PDF LaTeX documents **/ + /* document info */ abstract class Document_Name @@ -152,7 +273,10 @@ } - /* maintain chapter index -- NOT thread-safe */ + + /** HTML presentation **/ + + /* maintain chapter index */ private val sessions_path = Path.basic(".sessions") @@ -215,10 +339,10 @@ /* present session */ val session_graph_path = Path.explode("session_graph.pdf") - val readme_path = Path.basic("README.html") + val readme_path = Path.explode("README.html") + val files_path = Path.explode("files") def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html" - def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name) def token_markups(keywords: Keyword.Keywords, tok: Token): List[String] = { if (keywords.is_command(tok, Keyword.theory_end)) @@ -246,9 +370,11 @@ } def session_html( + resources: Resources, session: String, deps: Sessions.Deps, db_context: Sessions.Database_Context, + html_context: HTML_Context, presentation: Context) { val info = deps.sessions_structure(session) @@ -256,9 +382,8 @@ val base = deps(session) val session_dir = presentation.dir(db_context.store, info) - val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts")) - for (entry <- Isabelle_Fonts.fonts(hidden = true)) - File.copy(entry.path, session_fonts) + + html_context.init_fonts(session_dir) Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(options, base.session_graph_display)) @@ -300,6 +425,39 @@ HTML.link(prefix + html_name(name1), body) } + val files: List[XML.Body] = + { + var seen_files = List.empty[(Path, String, Document.Node.Name)] + (for { + thy_name <- base.session_theories.iterator + thy_command <- + Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator + snapshot = Document.State.init.snippet(thy_command) + (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator + if xml.nonEmpty + } yield { + val file_title = src_path.implode_short + val file_name = (files_path + src_path.squash.html).implode + + seen_files.find(p => p._1 == src_path || p._2 == file_name) match { + case None => seen_files ::= (src_path, file_name, thy_name) + case Some((_, _, thy_name1)) => + error("Incoherent use of file name " + src_path + " as " + quote(file_name) + + " in theory " + thy_name1 + " vs. " + thy_name) + } + + val file_path = session_dir + Path.explode(file_name) + html_context.init_fonts(file_path.dir) + + val title = "File " + Symbol.cartouche_decoded(file_title) + HTML.write_document(file_path.dir, file_path.file_name, + List(HTML.title(title)), + List(html_context.head(title), html_context.source(html_body(xml)))) + + List(HTML.link(file_name, HTML.text(file_title))) + }).toList + } + val theories = for (name <- base.session_theories) yield { @@ -334,7 +492,7 @@ val title = "Theory " + name.theory_base_name HTML.write_document(session_dir, html_name(name), List(HTML.title(title)), - HTML.div("head", List(HTML.chapter(title))) :: List(HTML.pre("source", thy_body))) + List(html_context.head(title), html_context.source(thy_body))) List(HTML.link(html_name(name), HTML.text(name.theory_base_name))) } @@ -342,104 +500,12 @@ val title = "Session " + session HTML.write_document(session_dir, "index.html", List(HTML.title(title + " (" + Distribution.version + ")")), - HTML.div("head", List(HTML.chapter(title), HTML.par(links))) :: - (if (theories.isEmpty) Nil - else List(HTML.div("theories", List(HTML.section("Theories"), HTML.itemize(theories)))))) - } - - - - /** 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.make_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) - } - } + html_context.head(title, List(HTML.par(links))) :: + html_context.contents("Theories", theories) ::: + html_context.contents("Files", files)) } - /* 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 **/ diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/Tools/build.scala Sun Dec 20 20:49:43 2020 +0100 @@ -502,11 +502,15 @@ val presentation_dir = presentation.dir(store) progress.echo("Presentation in " + presentation_dir.absolute) + val resources = Resources.empty + val html_context = Presentation.html_context() + using(store.open_database_context())(db_context => for ((_, (session_name, _)) <- presentation_chapters) { progress.expose_interrupt() progress.echo("Presenting " + session_name + " ...") - Presentation.session_html(session_name, deps, db_context, presentation) + Presentation.session_html( + resources, session_name, deps, db_context, html_context, presentation) }) val browser_chapters = diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Pure/Tools/build_job.scala Sun Dec 20 20:49:43 2020 +0100 @@ -30,8 +30,7 @@ (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { case (Value.Long(id), thy_file :: blobs_files) => - val thy_path = Path.explode(thy_file) - val node_name = resources.file_node(thy_path, theory = theory) + val node_name = resources.file_node(Path.explode(thy_file), theory = theory) val results = Command.Results.make( @@ -43,7 +42,7 @@ { val path = Path.explode(file) val name = resources.file_node(path) - val src_path = File.relative_path(thy_path, path).getOrElse(path) + val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) Command.Blob(name, src_path, None) }) val blobs_xml = @@ -94,7 +93,7 @@ { val store = Sessions.store(options) - val resources = new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) + val resources = Resources.empty val session = new Session(options, resources) using(store.open_database_context())(db_context => @@ -120,7 +119,7 @@ match { case None => progress.echo(thy_heading + " MISSING") case Some(command) => - val snapshot = Document.State.init.command_snippet(command) + val snapshot = Document.State.init.snippet(command) val rendering = new Rendering(snapshot, options, session) val messages = rendering.text_messages(Text.Range.full) @@ -376,7 +375,7 @@ export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false) - for ((xml, i) <- snapshot.xml_markup_blobs().zipWithIndex) { + for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { export(Export.MARKUP + (i + 1), xml) } export(Export.MARKUP, snapshot.xml_markup()) diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Tools/VSCode/src/preview_panel.scala Sun Dec 20 20:49:43 2020 +0100 @@ -30,8 +30,9 @@ 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 html_context = Presentation.html_context() + val document = Presentation.html_document(resources, snapshot, html_context) + channel.write(LSP.Preview_Response(file, column, document.title, document.content)) m - file } case None => m - file diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Tools/jEdit/src/document_model.scala Sun Dec 20 20:49:43 2020 +0100 @@ -16,7 +16,7 @@ import scala.collection.mutable import scala.annotation.tailrec -import org.gjt.sp.jedit.{jEdit, View} +import org.gjt.sp.jedit.View import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} @@ -153,11 +153,11 @@ state.change_result(st => st.buffer_models.get(buffer) match { case Some(buffer_model) if buffer_model.node_name == node_name => - buffer_model.init_token_marker + buffer_model.init_token_marker() (buffer_model, st) case _ => val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer) - buffer.propertiesChanged + buffer.propertiesChanged() res }) } @@ -168,7 +168,7 @@ state.change(st => if (st.buffer_models.isDefinedAt(buffer)) { val res = st.close_buffer(buffer) - buffer.propertiesChanged + buffer.propertiesChanged() res } else st) @@ -298,7 +298,7 @@ case Some(model) => val name = model.node_name val url = - PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" + + PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" + (if (plain_text) plain_text_prefix else "") + Url.encode(name.node) PIDE.editor.hyperlink_url(url).follow(view) case _ => @@ -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 html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root)) + val document = + Presentation.html_document(PIDE.resources, snapshot, html_context, 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) } } @@ -642,7 +643,7 @@ for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged"). invoke(text_area) - buffer.invalidateCachedFoldLevels + buffer.invalidateCachedFoldLevels() } def init_token_marker() diff -r eb1e5c4f70cd -r b7c9d6e48237 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Dec 19 17:49:14 2020 +0000 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Dec 20 20:49:43 2020 +0100 @@ -30,7 +30,7 @@ results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) = { val command = Command.rich_text(Document_ID.make(), results, formatted_body) - val snippet = snapshot.command_snippet(command) + val snippet = snapshot.snippet(command) val model = File_Model.empty(PIDE.session) val rendering = apply(snippet, model, PIDE.options.value) (command.source, rendering)