equal
deleted
inserted
replaced
250 new Nodes(graph3.map_node(name, _ => node)) |
250 new Nodes(graph3.map_node(name, _ => node)) |
251 } |
251 } |
252 |
252 |
253 def entries: Iterator[(Node.Name, Node)] = |
253 def entries: Iterator[(Node.Name, Node)] = |
254 graph.entries.map({ case (name, (node, _)) => (name, node) }) |
254 graph.entries.map({ case (name, (node, _)) => (name, node) }) |
|
255 |
|
256 def thy_load_commands(file_name: Node.Name): List[Command] = |
|
257 (for { |
|
258 (_, node) <- entries |
|
259 cmd <- node.thy_load_commands.iterator |
|
260 Exn.Res((name, _)) <- cmd.blobs.iterator |
|
261 if name == file_name |
|
262 } yield cmd).toList |
255 |
263 |
256 def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) |
264 def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) |
257 def topological_order: List[Node.Name] = graph.topological_order |
265 def topological_order: List[Node.Name] = graph.topological_order |
258 } |
266 } |
259 |
267 |