clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
clarified treatment of Session_Context.theory_names, added export_names;
clarified treatment of document_snapshot: sites on top of the session_stack;

--- a/src/Pure/PIDE/document.scala	Fri Aug 05 19:02:38 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 05 20:54:39 2022 +0200
@@ -633,8 +633,12 @@
     lazy val exports: List[Export.Entry] =
       state.node_exports(version, node_name).iterator.map(_._2).toList
 
-    lazy val exports_map: Map[String, Export.Entry] =
-      (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
+    lazy val all_exports: Map[Export.Entry_Name, Export.Entry] =
+      (for {
+        (name, _) <- version.nodes.iterator
+        (_, entry) <- state.node_exports(version, name).iterator
+        if entry.entry_name.session == Sessions.DRAFT
+      } yield entry.entry_name -> entry).toMap
 
 
     /* find command */

--- a/src/Pure/Thy/export.scala	Fri Aug 05 19:02:38 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 20:54:39 2022 +0200
@@ -306,8 +306,9 @@
             if name.is_theory && !resources.session_base.loaded_theory(name)
           } yield name.theory).toList
 
-        override def apply(export_name: String): Option[Entry] =
-          snapshot.exports_map.get(export_name)
+        override def apply(name: String): Option[Entry] =
+          snapshot.all_exports.get(
+            Entry_Name(session = Sessions.DRAFT, theory = snapshot.node_name.theory, name = name))
 
         override def focus(other_theory: String): Provider =
           if (other_theory == snapshot.node_name.theory) this
@@ -348,6 +349,7 @@
     def close(): Unit = ()
 
     lazy val theory_names: List[String] = read_theory_names(db, session)
+    lazy val entry_names: List[Entry_Name] = read_entry_names(db, session)
   }
 
   class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable {
@@ -356,13 +358,13 @@
     def open_session(
       session: String,
       resources: Resources,
-      snapshot: Document.Snapshot = Document.Snapshot.init
+      document_snapshot: Option[Document.Snapshot] = None
     ): Session_Context = {
       val session_hierarchy = resources.sessions_structure.build_hierarchy(session)
       db_context.database_server match {
         case Some(db) =>
           val session_databases = session_hierarchy.map(name => new Session_Database(name, db))
-          new Session_Context(resources, snapshot, db_context.cache, session_databases)
+          new Session_Context(resources, db_context.cache, session_databases, document_snapshot)
         case None =>
           val store = db_context.store
           val session_databases = {
@@ -378,8 +380,8 @@
                 store.bad_database(bad)
             }
           }
-          new Session_Context(resources, snapshot, db_context.cache, session_databases) {
-            override def close(): Unit = db_hierarchy.foreach(_.close())
+          new Session_Context(resources, db_context.cache, session_databases, document_snapshot) {
+            override def close(): Unit = session_databases.foreach(_.close())
           }
       }
     }
@@ -389,21 +391,62 @@
 
   class Session_Context private[Export](
     val resources: Resources,
-    val snapshot: Document.Snapshot,
     val cache: Term.Cache,
-    val db_hierarchy: List[Session_Database]
+    db_hierarchy: List[Session_Database],
+    document_snapshot: Option[Document.Snapshot]
   ) extends AutoCloseable {
     session_context =>
 
     def close(): Unit = ()
 
+    def session_name: String =
+      if (document_snapshot.isDefined) Sessions.DRAFT
+      else resources.session_base.session_name
+
+    def session_stack: List[String] =
+      ((if (document_snapshot.isDefined) List(session_name) else Nil) :::
+        db_hierarchy.map(_.session)).reverse
+
+    private def select[A](
+      session: String,
+      select1: Entry_Name => Option[A],
+      select2: Session_Database => List[A]
+    ): List[A] = {
+      def sel(name: String): List[A] =
+        if (name == Sessions.DRAFT) {
+          (for {
+            snapshot <- document_snapshot.iterator
+            entry_name <- snapshot.all_exports.keysIterator
+            res <- select1(entry_name).iterator
+          } yield entry_name -> res).toList.sortBy(_._1.compound_name).map(_._2)
+        }
+        else { db_hierarchy.find(_.session == name).map(select2).getOrElse(Nil) }
+      if (session.nonEmpty) sel(session) else session_stack.flatMap(sel)
+    }
+
+    def entry_names(session: String = session_name): List[Entry_Name] =
+      select(session, Some(_), _.entry_names)
+
+    def theory_names(session: String = session_name): List[String] =
+      select(session, a => if(a.name == THEORY_PARENTS) Some(a.theory) else None, _.theory_names)
+
     def get(theory: String, name: String): Option[Entry] =
-      snapshot.exports_map.get(name) orElse
+    {
+      def snapshot_entry =
+        for {
+          snapshot <- document_snapshot
+          entry_name = Entry_Name(session = Sessions.DRAFT, theory = theory, name = name)
+          entry <- snapshot.all_exports.get(entry_name)
+        } yield entry
+      def db_entry =
         db_hierarchy.view.map(session_db =>
           Export.Entry_Name(session = session_db.session, theory = theory, name = name)
             .read(session_db.db, cache))
           .collectFirst({ case Some(entry) => entry })
 
+      snapshot_entry orElse db_entry
+    }
+
     def apply(theory: String, name: String, permissive: Boolean = false): Entry =
       get(theory, name) match {
         case None if permissive => empty_entry(theory, name)
@@ -411,14 +454,11 @@
         case Some(entry) => entry
       }
 
-    def theory_names(session: String): List[String] =
-      db_hierarchy.find(_.session == session).map(_.theory_names).getOrElse(Nil)
-
     def theory(theory: String): Theory_Context =
       new Theory_Context(session_context, theory)
 
     override def toString: String =
-      "Export.Session_Context(" + commas_quote(db_hierarchy.map(_.session)) + ")"
+      "Export.Session_Context(" + commas_quote(session_stack) + ")"
   }
 
   class Theory_Context private[Export](session_context: Session_Context, theory: String) {