# HG changeset patch
# User wenzelm
# Date 1661450086 -7200
# Node ID d574b55c4e83e275803dc359e3d69a5289ea1f0a
# Parent  cec22f403c251a7eac4db835134cdcad332b5e16
read full sessions_requirements, for more complete entity hyperlinks;

diff -r cec22f403c25 -r d574b55c4e83 src/Pure/PIDE/document_info.scala
--- a/src/Pure/PIDE/document_info.scala	Thu Aug 25 19:36:33 2022 +0200
+++ b/src/Pure/PIDE/document_info.scala	Thu Aug 25 19:54:46 2022 +0200
@@ -87,7 +87,6 @@
     deps: Sessions.Deps,
     sessions: List[String]
   ): Document_Info = {
-    val sessions_domain = sessions.toSet
     val sessions_structure = deps.sessions_structure
     val sessions_requirements = sessions_structure.build_requirements(sessions)
 
@@ -99,20 +98,14 @@
       theory_context.files0(permissive = true) match {
         case Nil => None
         case files =>
-          val (entities, others) =
-            if (sessions_domain(session_name)) {
-              val theory = Export_Theory.read_theory(theory_context, permissive = true)
-              (theory.entity_iterator.toList,
-                theory.others.keySet.toList)
-            }
-            else (Nil, Nil)
+          val theory_export = Export_Theory.read_theory(theory_context, permissive = true)
           val theory =
             Theory(theory_name,
               static_session = sessions_structure.theory_qualifier(theory_name),
               dynamic_session = session_name,
               files = files,
-              entities = entities,
-              others = others)
+              entities = theory_export.entity_iterator.toList,
+              others = theory_export.others.keySet.toList)
           Some(theory)
       }
     }