217 if (qualifier == info.name) |
217 if (qualifier == info.name) |
218 Graph_Display.Node(name.theory_base_name, "theory." + name.theory) |
218 Graph_Display.Node(name.theory_base_name, "theory." + name.theory) |
219 else session_node(qualifier) |
219 else session_node(qualifier) |
220 } |
220 } |
221 |
221 |
222 val imports_subgraph = |
222 val required_sessions = |
223 sessions_structure.imports_graph. |
223 dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) |
224 restrict(sessions_structure.imports_graph.all_preds(info.deps).toSet) |
224 .map(theory => imports_base.theory_qualifier(theory)) |
|
225 .filterNot(_ == info.name) |
|
226 |
|
227 val required_subgraph = |
|
228 sessions_structure.imports_graph |
|
229 .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet) |
|
230 .transitive_closure |
|
231 .restrict(required_sessions.toSet) |
|
232 .transitive_reduction_acyclic |
225 |
233 |
226 val graph0 = |
234 val graph0 = |
227 (Graph_Display.empty_graph /: imports_subgraph.topological_order)( |
235 (Graph_Display.empty_graph /: required_subgraph.topological_order)( |
228 { case (g, session) => |
236 { case (g, session) => |
229 val a = session_node(session) |
237 val a = session_node(session) |
230 val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_)) |
238 val bs = required_subgraph.imm_preds(session).toList.map(session_node(_)) |
231 ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) |
239 ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) |
232 |
240 |
233 (graph0 /: dependencies.entries)( |
241 (graph0 /: dependencies.entries)( |
234 { case (g, entry) => |
242 { case (g, entry) => |
235 val a = node(entry.name) |
243 val a = node(entry.name) |