# HG changeset patch
# User wenzelm
# Date 1507656183 -7200
# Node ID 29ea2b900a0538c97019508c99291b3ef3514dbb
# Parent  3b50269b90c2e1c07c74ed5b01762c9380e59a98
tuned: each session has at most one defining entry;

diff -r 3b50269b90c2 -r 29ea2b900a05 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Tue Oct 10 13:46:12 2017 +0200
+++ b/src/Pure/Admin/afp.scala	Tue Oct 10 19:23:03 2017 +0200
@@ -46,15 +46,14 @@
   val entries_graph: Graph[String, Unit] =
   {
     val session_entries =
-      (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
-        (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
+      (Map.empty[String, String] /: entries) {
+        case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
       }
-    (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
-      val name1 = e1.name
-      val g1 = g.default_node(name1, ())
-      (g1 /: sessions_deps(e1)) { case (g2, s2) =>
-        (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
-          if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
+    (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
+      val e1 = entry.name
+      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s2) =>
+        (g1 /: session_entries.get(s2).filterNot(_ == e1)) { case (g2, e2) =>
+          g2.default_node(e2, ()).add_edge(e2, e1)
         }
       }
     }