# HG changeset patch
# User wenzelm
# Date 1608463481 -3600
# Node ID a093b8fc9e21d11ef8f53eae064c363c1d14dbda
# Parent  0d8bc0252e2ebe4c2ec476125a5c7c8080fb29f3
tuned signature: more explicit types;

diff -r 0d8bc0252e2e -r a093b8fc9e21 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Dec 19 15:32:29 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Sun Dec 20 12:24:41 2020 +0100
@@ -16,6 +16,22 @@
 
   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 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 */
 
@@ -70,24 +86,16 @@
   def html_document(
     resources: Resources,
     snapshot: Document.Snapshot,
-    plain_text: Boolean = false,
-    fonts_url: String => String = HTML.fonts_url()): HTML_Document =
+    context: HTML_Context,
+    plain_text: Boolean = false): 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)
+      val body = HTML.text(snapshot.node.source)
+      context.html_document(title, body)
     }
     else {
       resources.html_document(snapshot) match {
@@ -97,7 +105,7 @@
             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))
+          context.html_document(title, body)
       }
     }
   }
@@ -312,7 +320,8 @@
   /* 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)
diff -r 0d8bc0252e2e -r a093b8fc9e21 src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala	Sat Dec 19 15:32:29 2020 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Sun Dec 20 12:24:41 2020 +0100
@@ -30,7 +30,8 @@
               val snapshot = model.snapshot()
               if (snapshot.is_outdated) m
               else {
-                val document = Presentation.html_document(resources, snapshot)
+                val context = Presentation.html_context()
+                val document = Presentation.html_document(resources, snapshot, context)
                 channel.write(LSP.Preview_Response(file, column, document.title, document.content))
                 m - file
               }
diff -r 0d8bc0252e2e -r a093b8fc9e21 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Dec 19 15:32:29 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Dec 20 12:24:41 2020 +0100
@@ -319,9 +319,9 @@
         }
         yield {
           val snapshot = model.await_stable_snapshot()
+          val context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
           val document =
-            Presentation.html_document(PIDE.resources, snapshot,
-              fonts_url = HTML.fonts_dir(fonts_root),
+            Presentation.html_document(PIDE.resources, snapshot, context,
               plain_text = query.startsWith(plain_text_prefix))
           HTTP.Response.html(document.content)
         })