--- 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; }
--- 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 */
--- 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)
--- 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)
}
}
--- 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 */
--- 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"
-
--- 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
}
--- 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 */
--- 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 **/
--- 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 =
--- 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())
--- 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
--- 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()
--- 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)