# HG changeset patch # User wenzelm # Date 1636110690 -3600 # Node ID c492c8efcab474daf3337dd54885967b090ac1c6 # Parent 0554a5c4c191339a50a1e63b00b45c8681958d86 clarified HTML_Context: just one context type; diff -r 0554a5c4c191 -r c492c8efcab4 src/Pure/Thy/presentation.scala --- 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) diff -r 0554a5c4c191 -r c492c8efcab4 src/Pure/Tools/build.scala --- 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 =