98 } |
98 } |
99 val dep_files = Par_List.map(loaded _, rev_deps) |
99 val dep_files = Par_List.map(loaded _, rev_deps) |
100 ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } |
100 ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } |
101 } |
101 } |
102 |
102 |
|
103 def session_graph(parent_session: String, parent_base: Sessions.Base): Graph_Display.Graph = |
|
104 { |
|
105 val parent_session_node = |
|
106 Graph_Display.Node("[" + parent_session + "]", "session." + parent_session) |
|
107 |
|
108 def node(name: Document.Node.Name): Graph_Display.Node = |
|
109 if (parent_base.loaded_theory(name)) parent_session_node |
|
110 else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory) |
|
111 |
|
112 (Graph_Display.empty_graph /: deps) { |
|
113 case (g, dep) => |
|
114 if (parent_base.loaded_theory(dep.name)) g |
|
115 else { |
|
116 val a = node(dep.name) |
|
117 val bs = dep.header.imports.map({ case (name, _) => node(name) }) |
|
118 ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) |
|
119 } |
|
120 } |
|
121 } |
|
122 |
103 override def toString: String = deps.toString |
123 override def toString: String = deps.toString |
104 } |
124 } |
105 |
125 |
106 private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, |
126 private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, |
107 thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
127 thys: List[(Document.Node.Name, Position.T)]): Dependencies = |