16 { |
16 { |
17 /* session graph */ |
17 /* session graph */ |
18 |
18 |
19 def session_graph( |
19 def session_graph( |
20 parent_session: String, |
20 parent_session: String, |
21 parent_loaded: Document.Node.Name => Boolean, |
21 parent_base: Sessions.Base, |
22 deps: List[Thy_Info.Dep]): Graph_Display.Graph = |
22 deps: List[Thy_Info.Dep]): Graph_Display.Graph = |
23 { |
23 { |
24 val parent_session_node = |
24 val parent_session_node = |
25 Graph_Display.Node("[" + parent_session + "]", "session." + parent_session) |
25 Graph_Display.Node("[" + parent_session + "]", "session." + parent_session) |
26 |
26 |
27 def node(name: Document.Node.Name): Graph_Display.Node = |
27 def node(name: Document.Node.Name): Graph_Display.Node = |
28 if (parent_loaded(name)) parent_session_node |
28 if (parent_base.loaded_theory(name)) parent_session_node |
29 else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory) |
29 else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory) |
30 |
30 |
31 (Graph_Display.empty_graph /: deps) { |
31 (Graph_Display.empty_graph /: deps) { |
32 case (g, dep) => |
32 case (g, dep) => |
33 if (parent_loaded(dep.name)) g |
33 if (parent_base.loaded_theory(dep.name)) g |
34 else { |
34 else { |
35 val a = node(dep.name) |
35 val a = node(dep.name) |
36 val bs = dep.header.imports.map({ case (name, _) => node(name) }) |
36 val bs = dep.header.imports.map({ case (name, _) => node(name) }) |
37 ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) |
37 ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) |
38 } |
38 } |