# HG changeset patch
# User wenzelm
# Date 1636140367 -3600
# Node ID 84e8595a0ec77cbcff61ce804c59c2fec8f8f872
# Parent  909afe2361b1b7752b77ea52ff709262c102c8db
proper term_cache;

diff -r 909afe2361b1 -r 84e8595a0ec7 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 20:10:09 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 05 20:26:07 2021 +0100
@@ -27,6 +27,8 @@
 
   final class HTML_Context private[Presentation](fonts_url: String => String)
   {
+    val term_cache: Term.Cache = Term.Cache.make()
+
     private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
 
     def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
@@ -436,9 +438,9 @@
           else {
             html_context.cache_theory(thy_name,
               {
-                val provider =
-                  Export.Provider.database_context(db_context, hierarchy, thy_name)
-                Export_Theory.read_theory(provider, session, thy_name)
+                val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
+                Export_Theory.read_theory(
+                  provider, session, thy_name, cache = html_context.term_cache)
               })
         }
         thy_name -> theory