tuned: each session has at most one defining entry;
authorwenzelm
Tue Oct 10 19:23:03 2017 +0200 (22 months ago)
changeset 6683129ea2b900a05
parent 66830 3b50269b90c2
child 66832 875fe2cb7e70
tuned: each session has at most one defining entry;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Tue Oct 10 13:46:12 2017 +0200
     1.2 +++ b/src/Pure/Admin/afp.scala	Tue Oct 10 19:23:03 2017 +0200
     1.3 @@ -46,15 +46,14 @@
     1.4    val entries_graph: Graph[String, Unit] =
     1.5    {
     1.6      val session_entries =
     1.7 -      (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
     1.8 -        (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
     1.9 +      (Map.empty[String, String] /: entries) {
    1.10 +        case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
    1.11        }
    1.12 -    (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
    1.13 -      val name1 = e1.name
    1.14 -      val g1 = g.default_node(name1, ())
    1.15 -      (g1 /: sessions_deps(e1)) { case (g2, s2) =>
    1.16 -        (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
    1.17 -          if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
    1.18 +    (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
    1.19 +      val e1 = entry.name
    1.20 +      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s2) =>
    1.21 +        (g1 /: session_entries.get(s2).filterNot(_ == e1)) { case (g2, e2) =>
    1.22 +          g2.default_node(e2, ()).add_edge(e2, e1)
    1.23          }
    1.24        }
    1.25      }