41 /* dependency graph */ |
41 /* dependency graph */ |
42 |
42 |
43 private def sessions_deps(entry: AFP.Entry): List[String] = |
43 private def sessions_deps(entry: AFP.Entry): List[String] = |
44 entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted |
44 entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted |
45 |
45 |
46 val entries_graph: Graph[String, Unit] = |
46 def dependency_graph(acyclic: Boolean): Graph[String, Unit] = |
47 { |
47 { |
48 val session_entries = |
48 val session_entries = |
49 (Map.empty[String, String] /: entries) { |
49 (Map.empty[String, String] /: entries) { |
50 case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) } |
50 case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) } |
51 } |
51 } |
52 (Graph.empty[String, Unit] /: entries) { case (g, entry) => |
52 (Graph.empty[String, Unit] /: entries) { case (g, entry) => |
53 val e1 = entry.name |
53 val e1 = entry.name |
54 (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s2) => |
54 (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) => |
55 (g1 /: session_entries.get(s2).filterNot(_ == e1)) { case (g2, e2) => |
55 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) => |
56 g2.default_node(e2, ()).add_edge(e2, e1) |
56 val g3 = g2.default_node(e2, ()) |
|
57 if (acyclic) { |
|
58 try { g3.add_edge_acyclic(e2, e1) } |
|
59 catch { |
|
60 case exn: Graph.Cycles[_] => |
|
61 error(cat_lines(exn.cycles.map(cycle => |
|
62 "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") + |
|
63 " due to session " + quote(s)))) |
|
64 } |
|
65 } |
|
66 else g3.add_edge(e2, e1) |
57 } |
67 } |
58 } |
68 } |
59 } |
69 } |
60 } |
70 } |
|
71 |
|
72 val entries_graph: Graph[String, Unit] = dependency_graph(acyclic = false) |
61 |
73 |
62 def entries_graph_display: Graph_Display.Graph = |
74 def entries_graph_display: Graph_Display.Graph = |
63 Graph_Display.make_graph(entries_graph) |
75 Graph_Display.make_graph(entries_graph) |
64 |
76 |
65 def entries_json_text: String = |
77 def entries_json_text: String = |