--- 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 =>
--- 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) {
--- 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))
--- 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,