# HG changeset patch
# User wenzelm
# Date 1636189885 -3600
# Node ID bcca7e3bcd0d285f0751316b055004d4484a62d1
# Parent  eb89b3a378260f844f54dadb890f823f445a2c45
proper treatment of session build hierarchy;

diff -r eb89b3a37826 -r bcca7e3bcd0d src/Pure/Thy/presentation.scala
--- 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 =
diff -r eb89b3a37826 -r bcca7e3bcd0d src/Pure/Tools/build_job.scala
--- 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) =>
diff -r eb89b3a37826 -r bcca7e3bcd0d src/Pure/Tools/profiling_report.scala
--- 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