# HG changeset patch
# User wenzelm
# Date 1637589817 -3600
# Node ID 46c7fafbea3d3efb0bc42938a26ac34ca8a8355e
# Parent  c1b5d6e6ff74432b6314ae9e682ccfed55cd91f0
more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory;

diff -r c1b5d6e6ff74 -r 46c7fafbea3d src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Nov 21 17:42:11 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Mon Nov 22 15:03:37 2021 +0100
@@ -94,15 +94,6 @@
       locale_dependencies.iterator.map(_.no_content) ++
       (for { (_, xs) <- others; x <- xs.iterator } yield x.no_content)
 
-    lazy val entity_by_range: Map[Symbol.Range, List[Entity[No_Content]]] =
-      entity_iterator.toList.groupBy(_.range)
-
-    lazy val entity_by_kind_name: Map[(String, String), Entity[No_Content]] =
-      entity_iterator.map(entity => ((entity.kind, entity.name), entity)).toMap
-
-    lazy val entity_kinds: Set[String] =
-      entity_iterator.map(_.kind).toSet
-
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
         parents.map(cache.string),
diff -r c1b5d6e6ff74 -r 46c7fafbea3d src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sun Nov 21 17:42:11 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Mon Nov 22 15:03:37 2021 +0100
@@ -34,9 +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)
+    type Theory_Exports = Map[String, Entity_Context.Theory_Export]
+    def theory_exports: Theory_Exports = Map.empty
+    def theory_export(name: String): Entity_Context.Theory_Export =
+      theory_exports.getOrElse(name, Entity_Context.no_theory_export)
 
 
     /* HTML content */
@@ -94,6 +95,13 @@
 
   object Entity_Context
   {
+    sealed case class Theory_Export(
+      entity_by_range: Map[Symbol.Range, List[Export_Theory.Entity[Export_Theory.No_Content]]],
+      entity_by_kind_name: Map[(String, String), Export_Theory.Entity[Export_Theory.No_Content]],
+      others: List[String])
+
+    val no_theory_export: Theory_Export = Theory_Export(Map.empty, Map.empty, Nil)
+
     object Theory_Ref
     {
       def unapply(props: Properties.T): Option[Document.Node.Name] =
@@ -471,7 +479,7 @@
   def read_exports(
     sessions: List[String],
     deps: Sessions.Deps,
-    db_context: Sessions.Database_Context): Map[String, Export_Theory.Theory] =
+    db_context: Sessions.Database_Context): Map[String, Entity_Context.Theory_Export] =
   {
     type Batch = (String, List[String])
     val batches =
@@ -480,7 +488,7 @@
             val thys = deps(session).loaded_theories.keys.filterNot(seen)
             (seen ++ thys, (session, thys) :: batches)
         })._2
-    Par_List.map[Batch, List[(String, Export_Theory.Theory)]](
+    Par_List.map[Batch, List[(String, Entity_Context.Theory_Export)]](
       { case (session, thys) =>
           for (thy_name <- thys) yield {
             val theory =
@@ -492,9 +500,14 @@
                 }
                 else Export_Theory.no_theory
               }
-            thy_name -> theory
+            val entity_by_range =
+              theory.entity_iterator.toList.groupBy(_.range)
+            val entity_by_kind_name =
+              theory.entity_iterator.map(entity => ((entity.kind, entity.name), entity)).toMap
+            val others = theory.others.keySet.toList
+            thy_name -> Entity_Context.Theory_Export(entity_by_range, entity_by_kind_name, others)
           }
-      }, batches).iterator.flatten.toMap
+      }, batches).flatten.toMap
   }
 
   def session_html(
@@ -578,7 +591,7 @@
 
         val thy_elements =
           session_elements.copy(entity =
-            html_context.theory_export(name.theory).others.keySet
+            html_context.theory_export(name.theory).others
               .foldLeft(session_elements.entity)(_ + _))
 
         val files_html =
diff -r c1b5d6e6ff74 -r 46c7fafbea3d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Nov 21 17:42:11 2021 +0100
+++ b/src/Pure/Tools/build.scala	Mon Nov 22 15:03:37 2021 +0100
@@ -521,7 +521,7 @@
                 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
+                override def theory_exports: Theory_Exports = exports
               }
             Presentation.session_html(
               session, deps, db_context, progress = progress,