--- a/src/Pure/Thy/presentation.scala Sat Nov 06 00:13:29 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Sat Nov 06 10:11:25 2021 +0100
@@ -26,10 +26,13 @@
{
val term_cache: Term.Cache = Term.Cache.make()
- private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
+ 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)))
- def cached_theories: Set[String] = theory_cache.value.keySet
-
+ 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 =>
@@ -429,9 +432,8 @@
map(link => HTML.text("View ") ::: List(link))).flatten
}
- val cached_theories: Set[String] = html_context.cached_theories
val all_used_theories = hierarchy.flatMap(a => deps(a).used_theories.map(_._1))
- val present_theories = all_used_theories.filterNot(name => cached_theories.contains(name.theory))
+ val present_theories = html_context.register_presented(all_used_theories)
val theory_exports: Map[String, Export_Theory.Theory] =
(for (node <- all_used_theories.iterator) yield {
@@ -537,10 +539,10 @@
def read_theory(name: Document.Node.Name): Option[Theory] =
{
progress.expose_interrupt()
- if (verbose) progress.echo("Presenting theory " + name)
- for (command <- Build_Job.read_theory(db_context, resources, session, name.theory))
+ for (command <- Build_Job.read_theory(db_context, resources, hierarchy, name.theory))
yield {
+ if (verbose) progress.echo("Presenting theory " + name)
val snapshot = Document.State.init.snippet(command)
val files_html =
--- a/src/Pure/Tools/build_job.scala Sat Nov 06 00:13:29 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Nov 06 10:11:25 2021 +0100
@@ -19,12 +19,12 @@
def read_theory(
db_context: Sessions.Database_Context,
resources: Resources,
- session: String,
+ session_hierarchy: List[String],
theory: String,
unicode_symbols: Boolean = false): Option[Command] =
{
def read(name: String): Export.Entry =
- db_context.get_export(List(session), theory, name)
+ db_context.get_export(session_hierarchy, theory, name)
def read_xml(name: String): XML.Body =
YXML.parse_body(
@@ -118,7 +118,8 @@
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
for (thy <- print_theories) {
val thy_heading = "\nTheory " + quote(thy) + ":"
- read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols)
+ read_theory(db_context, resources, List(session_name), thy,
+ unicode_symbols = unicode_symbols)
match {
case None => progress.echo(thy_heading + " MISSING")
case Some(command) =>
--- a/src/Pure/Tools/profiling_report.scala Sat Nov 06 00:13:29 2021 +0100
+++ b/src/Pure/Tools/profiling_report.scala Sat Nov 06 10:11:25 2021 +0100
@@ -11,21 +11,20 @@
{
def profiling_report(
options: Options,
- session_name: String,
+ session: String,
theories: List[String] = Nil,
clean_name: Boolean = false,
progress: Progress = new Progress): Unit =
{
val store = Sessions.store(options)
val resources = Resources.empty
- val session = new Session(options, resources)
using(store.open_database_context())(db_context =>
{
val result =
- db_context.input_database(session_name)((db, name) => Some(store.read_theories(db, name)))
+ db_context.input_database(session)((db, name) => Some(store.read_theories(db, name)))
result match {
- case None => error("Missing build database for session " + quote(session_name))
+ case None => error("Missing build database for session " + quote(session))
case Some(used_theories) =>
theories.filterNot(used_theories.toSet) match {
case Nil =>
@@ -35,7 +34,7 @@
(for {
thy <- used_theories.iterator
if theories.isEmpty || theories.contains(thy)
- command <- Build_Job.read_theory(db_context, resources, session_name, thy).iterator
+ command <- Build_Job.read_theory(db_context, resources, List(session), thy).iterator
snapshot = Document.State.init.snippet(command)
(Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
} yield if (clean_name) report.clean_name else report).toList