tuned; draft
authorFabian Huch <huch@in.tum.de>
Wed, 29 Sep 2021 09:34:15 +0200
changeset 74746 7d71fb119ffa
parent 74744 a6b85db273e1
tuned;
src/Pure/Thy/presentation.scala
src/Pure/Tools/build.scala
--- 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 =