diff -r e3fb3036a00e -r b5740579cad6 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Tue Apr 04 23:21:16 2017 +0200 +++ b/src/Pure/Thy/present.scala Wed Apr 05 11:39:36 2017 +0200 @@ -18,19 +18,19 @@ def session_graph( parent_session: String, - parent_loaded: Document.Node.Name => Boolean, + parent_base: Sessions.Base, deps: List[Thy_Info.Dep]): Graph_Display.Graph = { val parent_session_node = Graph_Display.Node("[" + parent_session + "]", "session." + parent_session) def node(name: Document.Node.Name): Graph_Display.Node = - if (parent_loaded(name)) parent_session_node + if (parent_base.loaded_theory(name)) parent_session_node else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory) (Graph_Display.empty_graph /: deps) { case (g, dep) => - if (parent_loaded(dep.name)) g + if (parent_base.loaded_theory(dep.name)) g else { val a = node(dep.name) val bs = dep.header.imports.map({ case (name, _) => node(name) })