# HG changeset patch
# User wenzelm
# Date 1636720595 -3600
# Node ID 0579ff142613047230f3ed60b4959dd79b237ee8
# Parent  71a447e4073b290fa9fad2210704d5235a86514a
clarified signature;

diff -r 71a447e4073b -r 0579ff142613 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 12 13:02:20 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 12 13:36:35 2021 +0100
@@ -20,11 +20,10 @@
 
   sealed case class HTML_Document(title: String, content: String)
 
-  def html_context(cache: Term.Cache = Term.Cache.make()): HTML_Context =
-    new HTML_Context(cache)
+  class HTML_Context
+  {
+    val cache: Term.Cache = Term.Cache.make()
 
-  final class HTML_Context private[Presentation](val cache: Term.Cache)
-  {
     private val already_presented = Synchronized(Set.empty[String])
     def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
       already_presented.change_result(presented =>
diff -r 71a447e4073b -r 0579ff142613 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Nov 12 13:02:20 2021 +0100
+++ b/src/Pure/Tools/build.scala	Fri Nov 12 13:36:35 2021 +0100
@@ -506,7 +506,8 @@
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
-        val html_context = Presentation.html_context(cache = store.cache)
+        val html_context =
+          new Presentation.HTML_Context { override val cache: Term.Cache = store.cache }
 
         using(store.open_database_context())(db_context =>
           for (info <- presentation_sessions) {
diff -r 71a447e4073b -r 0579ff142613 src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala	Fri Nov 12 13:02:20 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Nov 12 13:36:35 2021 +0100
@@ -31,7 +31,7 @@
                 val snapshot = model.snapshot()
                 if (snapshot.is_outdated) m
                 else {
-                  val html_context = Presentation.html_context()
+                  val html_context = new Presentation.HTML_Context
                   val document =
                     Presentation.html_document(snapshot, html_context, Presentation.elements2)
                   channel.write(LSP.Preview_Response(file, column, document.title, document.content))
diff -r 71a447e4073b -r 0579ff142613 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Nov 12 13:02:20 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Nov 12 13:36:35 2021 +0100
@@ -324,7 +324,7 @@
         }
         yield {
           val snapshot = model.await_stable_snapshot()
-          val html_context = Presentation.html_context()
+          val html_context = new Presentation.HTML_Context
           val document =
             Presentation.html_document(
               snapshot, html_context, Presentation.elements2,