--- a/src/Pure/Thy/presentation.scala Tue Sep 28 11:30:14 2021 +0200
+++ b/src/Pure/Thy/presentation.scala Wed Sep 29 09:34:15 2021 +0200
@@ -423,7 +423,8 @@
verbose: Boolean = false,
html_context: HTML_Context,
elements: Elements,
- presentation: Context): Unit =
+ presentation: Context,
+ cache: Term.Cache = Term.Cache.none): Unit =
{
val info = deps.sessions_structure(session)
val options = info.options
@@ -475,7 +476,7 @@
val provider = Export.Provider.database_context(db_context, List(session1), name.theory)
provider(Export.THEORY_PREFIX + "parents") match {
case Some(_) =>
- val theory = Export_Theory.read_theory(provider, session1, name.theory)
+ val theory = Export_Theory.read_theory(provider, session1, name.theory, cache)
theory.entity_iterator.toVector
case None =>
progress.echo_error_message("No exports for: " + name)
--- a/src/Pure/Tools/build.scala Tue Sep 28 11:30:14 2021 +0200
+++ b/src/Pure/Tools/build.scala Wed Sep 29 09:34:15 2021 +0200
@@ -501,6 +501,7 @@
val resources = Resources.empty
val html_context = Presentation.html_context()
+ val cache = Term.Cache.make()
using(store.open_database_context())(db_context =>
for ((_, (session_name, _)) <- presentation_chapters) {
@@ -509,7 +510,7 @@
Presentation.session_html(
resources, session_name, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
- elements = Presentation.elements1, presentation = presentation)
+ elements = Presentation.elements1, presentation = presentation, cache)
})
val browser_chapters =