# HG changeset patch # User wenzelm # Date 1637178549 -3600 # Node ID 3064e165c66065f38a61c799c1d2d38c8e414b1f # Parent 1fd8705503b4b197ea695f89d6f737a3738281c8 clarified HTML_Context.theory_exports: prefer value-oriented parallelism; diff -r 1fd8705503b4 -r 3064e165c660 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Wed Nov 17 15:09:10 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Wed Nov 17 20:49:09 2021 +0100 @@ -22,7 +22,7 @@ abstract class HTML_Context { - /* directory structure */ + /* directory structure and resources */ def root_dir: Path def theory_session(name: Document.Node.Name): Sessions.Info @@ -34,6 +34,10 @@ def files_path(name: Document.Node.Name, path: Path): Path = theory_path(name).dir + Path.explode("files") + path.squash.html + def theory_exports: Map[String, Export_Theory.Theory] = Map.empty + def theory_export(name: String): Export_Theory.Theory = + theory_exports.getOrElse(name, Export_Theory.no_theory) + /* HTML content */ @@ -64,33 +68,6 @@ } - /* presentation state */ - - class State - { - /* 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.value.get(thy_name) match { - case Some(thy) => thy - case None => - val thy1 = make_thy - theory_cache.change_result(thys => - { - thys.get(thy_name) match { - case Some(thy) => (thy, thys) - case None => (thy1, thys + (thy_name -> thy1)) - } - }) - } - } - } - - /* presentation elements */ sealed case class Elements( @@ -145,7 +122,7 @@ session: String, deps: Sessions.Deps, node: Document.Node.Name, - theory_exports: Map[String, Export_Theory.Theory]): Entity_Context = + html_context: HTML_Context): Entity_Context = new Entity_Context { private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty @@ -156,7 +133,8 @@ case _ => Some { val entities = - theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range)) + html_context.theory_exports.get(node.theory) + .flatMap(_.entity_by_range.get(range)) .getOrElse(Nil) val body1 = if (seen_ranges.contains(range)) { @@ -186,7 +164,7 @@ private def logical_ref(thy_name: String, kind: String, name: String): Option[String] = for { - thy <- theory_exports.get(thy_name) + thy <- html_context.theory_exports.get(thy_name) entity <- thy.entity_by_kind_name.get((kind, name)) } yield entity.kname @@ -490,6 +468,35 @@ else None } + def read_exports( + sessions: List[String], + deps: Sessions.Deps, + db_context: Sessions.Database_Context): Map[String, Export_Theory.Theory] = + { + type Batch = (String, List[String]) + val batches = + sessions.foldLeft((Set.empty[String], List.empty[Batch]))( + { case ((seen, batches), session) => + val thys = deps(session).loaded_theories.keys.filterNot(seen) + (seen ++ thys, (session, thys) :: batches) + })._2 + Par_List.map[Batch, List[(String, Export_Theory.Theory)]]( + { case (session, thys) => + for (thy_name <- thys) yield { + val theory = + if (thy_name == Thy_Header.PURE) Export_Theory.no_theory + else { + val provider = Export.Provider.database_context(db_context, List(session), thy_name) + if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) { + Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache) + } + else Export_Theory.no_theory + } + thy_name -> theory + } + }, batches).iterator.flatten.toMap + } + def session_html( session: String, deps: Sessions.Deps, @@ -497,7 +504,6 @@ progress: Progress = new Progress, verbose: Boolean = false, html_context: HTML_Context, - state: State, session_elements: Elements): Unit = { val info = deps.sessions_structure(session) @@ -544,27 +550,8 @@ map(link => HTML.text("View ") ::: List(link))).flatten } - val theory_exports: Map[String, Export_Theory.Theory] = - (for (node <- hierarchy_theories.iterator) yield { - val thy_name = node.theory - val theory = - if (thy_name == Thy_Header.PURE) Export_Theory.no_theory - else { - 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 = state.cache) - } - else Export_Theory.no_theory - }) - } - thy_name -> theory - }).toMap - def entity_context(name: Document.Node.Name): Entity_Context = - Entity_Context.make(session, deps, name, theory_exports) + Entity_Context.make(session, deps, name, html_context) sealed case class Seen_File( @@ -591,7 +578,8 @@ val thy_elements = session_elements.copy(entity = - theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _)) + html_context.theory_export(name.theory).others.keySet + .foldLeft(session_elements.entity)(_ + _)) val files_html = for { diff -r 1fd8705503b4 -r 3064e165c660 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Nov 17 15:09:10 2021 +0100 +++ b/src/Pure/Tools/build.scala Wed Nov 17 20:49:09 2021 +0100 @@ -506,9 +506,11 @@ 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 => + { + val exports = + Presentation.read_exports(presentation_sessions.map(_.name), deps, db_context) - using(store.open_database_context())(db_context => Par_List.map((session: String) => { progress.expose_interrupt() @@ -519,12 +521,14 @@ 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)) + override def theory_exports: Map[String, Export_Theory.Theory] = exports } Presentation.session_html( session, deps, db_context, progress = progress, - verbose = verbose, html_context = html_context, state = state, + verbose = verbose, html_context = html_context, Presentation.elements1) - }, presentation_sessions.map(_.name))) + }, presentation_sessions.map(_.name)) + }) } }