cycle check with informative error;
authorwenzelm
Tue Oct 10 19:48:29 2017 +0200 (19 months ago)
changeset 66832875fe2cb7e70
parent 66831 29ea2b900a05
child 66833 091012ac3dc2
cycle check with informative error;
src/Pure/Admin/afp.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Tue Oct 10 19:23:03 2017 +0200
     1.2 +++ b/src/Pure/Admin/afp.scala	Tue Oct 10 19:48:29 2017 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    private def sessions_deps(entry: AFP.Entry): List[String] =
     1.5      entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
     1.6  
     1.7 -  val entries_graph: Graph[String, Unit] =
     1.8 +  def dependency_graph(acyclic: Boolean): Graph[String, Unit] =
     1.9    {
    1.10      val session_entries =
    1.11        (Map.empty[String, String] /: entries) {
    1.12 @@ -51,14 +51,26 @@
    1.13        }
    1.14      (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
    1.15        val e1 = entry.name
    1.16 -      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s2) =>
    1.17 -        (g1 /: session_entries.get(s2).filterNot(_ == e1)) { case (g2, e2) =>
    1.18 -          g2.default_node(e2, ()).add_edge(e2, e1)
    1.19 +      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
    1.20 +        (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
    1.21 +          val g3 = g2.default_node(e2, ())
    1.22 +          if (acyclic) {
    1.23 +            try { g3.add_edge_acyclic(e2, e1) }
    1.24 +            catch {
    1.25 +              case exn: Graph.Cycles[_] =>
    1.26 +                error(cat_lines(exn.cycles.map(cycle =>
    1.27 +                  "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
    1.28 +                  " due to session " + quote(s))))
    1.29 +            }
    1.30 +          }
    1.31 +          else g3.add_edge(e2, e1)
    1.32          }
    1.33        }
    1.34      }
    1.35    }
    1.36  
    1.37 +  val entries_graph: Graph[String, Unit] = dependency_graph(acyclic = false)
    1.38 +
    1.39    def entries_graph_display: Graph_Display.Graph =
    1.40      Graph_Display.make_graph(entries_graph)
    1.41