just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);
--- a/src/Pure/Thy/presentation.scala Tue Nov 16 18:45:31 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Tue Nov 16 21:21:15 2021 +0100
@@ -35,31 +35,6 @@
theory_path(name).dir + Path.explode("files") + path.squash.html
- /* cached theory exports */
-
- val cache: Term.Cache = Term.Cache.make()
-
- private val already_presented = Synchronized(Set.empty[String])
- def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
- already_presented.change_result(presented =>
- (nodes.filterNot(name => presented.contains(name.theory)),
- presented ++ nodes.iterator.map(_.theory)))
-
- 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))
- }
- })
- }
-
-
/* HTML content */
def head(title: String, rest: XML.Body = Nil): XML.Tree =
@@ -89,6 +64,40 @@
}
+ /* presentation state */
+
+ class State
+ {
+ /* already presented theories */
+
+ private val already_presented = Synchronized(Set.empty[String])
+
+ def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
+ already_presented.change_result(presented =>
+ (nodes.filterNot(name => presented.contains(name.theory)),
+ presented ++ nodes.iterator.map(_.theory)))
+
+
+ /* cached theory exports */
+
+ val 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 =
+ {
+ 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))
+ }
+ })
+ }
+ }
+
+
/* presentation elements */
sealed case class Elements(
@@ -495,6 +504,7 @@
progress: Progress = new Progress,
verbose: Boolean = false,
html_context: HTML_Context,
+ state: State,
session_elements: Elements): Unit =
{
val info = deps.sessions_structure(session)
@@ -547,12 +557,12 @@
val theory =
if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
else {
- html_context.cache_theory(thy_name,
+ state.cache_theory(thy_name,
{
val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
Export_Theory.read_theory(
- provider, session, thy_name, cache = html_context.cache)
+ provider, session, thy_name, cache = state.cache)
}
else Export_Theory.no_theory
})
@@ -645,7 +655,7 @@
})
}
- val theories = html_context.register_presented(hierarchy_theories).flatMap(present_theory)
+ val theories = state.register_presented(hierarchy_theories).flatMap(present_theory)
val title = "Session " + session
HTML.write_document(session_dir, "index.html",
--- a/src/Pure/Tools/build.scala Tue Nov 16 18:45:31 2021 +0100
+++ b/src/Pure/Tools/build.scala Tue Nov 16 21:21:15 2021 +0100
@@ -506,6 +506,8 @@
Presentation.update_chapter(presentation_dir, chapter, entries)
}
+ val state = new Presentation.State { override val cache: Term.Cache = store.cache }
+
using(store.open_database_context())(db_context =>
for (session <- presentation_sessions.map(_.name)) {
progress.expose_interrupt()
@@ -513,14 +515,13 @@
val html_context =
new Presentation.HTML_Context {
- override val cache: Term.Cache = store.cache
override def root_dir: Path = presentation_dir
override def theory_session(name: Document.Node.Name): Sessions.Info =
deps.sessions_structure(deps(session).theory_qualifier(name))
}
Presentation.session_html(
session, deps, db_context, progress = progress,
- verbose = verbose, html_context = html_context,
+ verbose = verbose, html_context = html_context, state = state,
Presentation.elements1)
})
}