# HG changeset patch
# User wenzelm
# Date 1637158995 -3600
# Node ID 2ad892ac749acefa1e7015d635168619d2d109aa
# Parent  4543fb2b5ef24bdda546f56caa2f9dbd68d4048e
present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
eliminated implicit state: these theories are globally unique;

diff -r 4543fb2b5ef2 -r 2ad892ac749a src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 17 13:11:58 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 17 15:23:15 2021 +0100
@@ -68,16 +68,6 @@
 
   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()
@@ -655,7 +645,7 @@
       })
     }
 
-    val theories = state.register_presented(hierarchy_theories).flatMap(present_theory)
+    val theories = base.session_theories.flatMap(present_theory)
 
     val title = "Session " + session
     HTML.write_document(session_dir, "index.html",
diff -r 4543fb2b5ef2 -r 2ad892ac749a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 17 13:11:58 2021 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 17 15:23:15 2021 +0100
@@ -244,7 +244,7 @@
 
     val presentation_sessions =
       (for {
-        session_name <- deps.sessions_structure.imports_topological_order.iterator
+        session_name <- deps.sessions_structure.build_topological_order.iterator
         info <- deps.sessions_structure.get(session_name)
         if full_sessions_selected(session_name) && presentation.enabled(info) }
       yield info).toList