# HG changeset patch
# User wenzelm
# Date 1507657709 -7200
# Node ID 875fe2cb7e706bdc0eccacff8cf2c30ca5a9dccf
# Parent  29ea2b900a0538c97019508c99291b3ef3514dbb
cycle check with informative error;

diff -r 29ea2b900a05 -r 875fe2cb7e70 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Tue Oct 10 19:23:03 2017 +0200
+++ b/src/Pure/Admin/afp.scala	Tue Oct 10 19:48:29 2017 +0200
@@ -43,7 +43,7 @@
   private def sessions_deps(entry: AFP.Entry): List[String] =
     entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
 
-  val entries_graph: Graph[String, Unit] =
+  def dependency_graph(acyclic: Boolean): Graph[String, Unit] =
   {
     val session_entries =
       (Map.empty[String, String] /: entries) {
@@ -51,14 +51,26 @@
       }
     (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)
+      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
+        (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
+          val g3 = g2.default_node(e2, ())
+          if (acyclic) {
+            try { g3.add_edge_acyclic(e2, e1) }
+            catch {
+              case exn: Graph.Cycles[_] =>
+                error(cat_lines(exn.cycles.map(cycle =>
+                  "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
+                  " due to session " + quote(s))))
+            }
+          }
+          else g3.add_edge(e2, e1)
         }
       }
     }
   }
 
+  val entries_graph: Graph[String, Unit] = dependency_graph(acyclic = false)
+
   def entries_graph_display: Graph_Display.Graph =
     Graph_Display.make_graph(entries_graph)