merged
authorwenzelm
Sun, 20 Dec 2020 20:49:43 +0100
changeset 73205 b7c9d6e48237
parent 73194 eb1e5c4f70cd (current diff)
parent 73204 2621225b4bdd (diff)
child 73206 f931a2a68ab8
merged
--- 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)