--- a/src/Pure/Thy/presentation.scala Fri Nov 05 12:05:17 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Fri Nov 05 12:11:30 2021 +0100
@@ -27,6 +27,21 @@
final class HTML_Context private[Presentation](fonts_url: String => String)
{
+ 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 =
+ {
+ theory_cache.change_result(thys =>
+ {
+ thys.get(thy_name) match {
+ case Some(thy) => (thy, thys)
+ case None =>
+ val thy = make_thy
+ (thy, thys + (thy_name -> thy))
+ }
+ })
+ }
+
def init_fonts(dir: Path): Unit =
{
val fonts_dir = Isabelle_System.make_directory(dir + fonts_path)
@@ -328,32 +343,6 @@
}
- /* theory cache */
-
- object Theory_Cache
- {
- def apply(): Theory_Cache = new Theory_Cache()
- }
-
- class Theory_Cache private()
- {
- private val cache = Synchronized(Map.empty[String, Export_Theory.Theory])
-
- def apply(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
- {
- cache.change_result(thys =>
- {
- thys.get(thy_name) match {
- case Some(thy) => (thy, thys)
- case None =>
- val thy = make_thy
- (thy, thys + (thy_name -> thy))
- }
- })
- }
- }
-
-
/* present session */
val session_graph_path = Path.explode("session_graph.pdf")
@@ -402,8 +391,7 @@
verbose: Boolean = false,
html_context: HTML_Context,
elements: Elements,
- presentation: Context,
- theory_cache: Theory_Cache = Theory_Cache()): Unit =
+ presentation: Context): Unit =
{
val info = deps.sessions_structure(session)
val options = info.options
@@ -449,7 +437,7 @@
def read_theory(thy_name: String): Export_Theory.Theory =
if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
else {
- theory_cache(thy_name,
+ html_context.cache_theory(thy_name,
{
val qualifier = deps(session).theory_qualifier(thy_name)
val provider = Export.Provider.database_context(db_context, List(qualifier), thy_name)
--- a/src/Pure/Tools/build.scala Fri Nov 05 12:05:17 2021 +0100
+++ b/src/Pure/Tools/build.scala Fri Nov 05 12:11:30 2021 +0100
@@ -501,7 +501,6 @@
val resources = Resources.empty
val html_context = Presentation.html_context()
- val theory_cache = Presentation.Theory_Cache()
using(store.open_database_context())(db_context =>
for ((_, (session_name, _)) <- presentation_chapters) {
@@ -510,8 +509,7 @@
Presentation.session_html(
resources, session_name, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
- elements = Presentation.elements1, presentation = presentation,
- theory_cache = theory_cache)
+ elements = Presentation.elements1, presentation = presentation)
})
val browser_chapters =