# HG changeset patch
# User wenzelm
# Date 1572023316 -7200
# Node ID b62bb9a61abc2b041fef6d3bb6c63f176dd97cef
# Parent  420f5d1953c7a52a157aac38229ce865f380a327# Parent  79d23e6436d0632844f35641401e09eebbb113dd
merged

diff -r 420f5d1953c7 -r b62bb9a61abc src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Oct 25 16:56:47 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Oct 25 19:08:36 2019 +0200
@@ -219,15 +219,23 @@
                 else session_node(qualifier)
               }
 
-              val imports_subgraph =
-                sessions_structure.imports_graph.
-                  restrict(sessions_structure.imports_graph.all_preds(info.deps).toSet)
+              val required_sessions =
+                dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory))
+                  .map(theory => imports_base.theory_qualifier(theory))
+                  .filterNot(_ == info.name)
+
+              val required_subgraph =
+                sessions_structure.imports_graph
+                  .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet)
+                  .transitive_closure
+                  .restrict(required_sessions.toSet)
+                  .transitive_reduction_acyclic
 
               val graph0 =
-                (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
+                (Graph_Display.empty_graph /: required_subgraph.topological_order)(
                   { case (g, session) =>
                       val a = session_node(session)
-                      val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
+                      val bs = required_subgraph.imm_preds(session).toList.map(session_node(_))
                       ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
 
               (graph0 /: dependencies.entries)(