merged
authorwenzelm
Tue Oct 10 19:51:54 2017 +0200 (19 months ago)
changeset 66833091012ac3dc2
parent 66827 c94531b5007d
parent 66832 875fe2cb7e70
child 66834 c925393ae6b9
merged
     1.1 --- a/src/Pure/Admin/afp.scala	Tue Oct 10 17:15:37 2017 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Tue Oct 10 19:51:54 2017 +0200
     1.3 @@ -43,23 +43,34 @@
     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 -      (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
    1.12 -        (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
    1.13 +      (Map.empty[String, String] /: entries) {
    1.14 +        case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
    1.15        }
    1.16 -    (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
    1.17 -      val name1 = e1.name
    1.18 -      val g1 = g.default_node(name1, ())
    1.19 -      (g1 /: sessions_deps(e1)) { case (g2, s2) =>
    1.20 -        (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
    1.21 -          if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
    1.22 +    (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
    1.23 +      val e1 = entry.name
    1.24 +      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
    1.25 +        (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
    1.26 +          val g3 = g2.default_node(e2, ())
    1.27 +          if (acyclic) {
    1.28 +            try { g3.add_edge_acyclic(e2, e1) }
    1.29 +            catch {
    1.30 +              case exn: Graph.Cycles[_] =>
    1.31 +                error(cat_lines(exn.cycles.map(cycle =>
    1.32 +                  "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
    1.33 +                  " due to session " + quote(s))))
    1.34 +            }
    1.35 +          }
    1.36 +          else g3.add_edge(e2, e1)
    1.37          }
    1.38        }
    1.39      }
    1.40    }
    1.41  
    1.42 +  val entries_graph: Graph[String, Unit] = dependency_graph(acyclic = false)
    1.43 +
    1.44    def entries_graph_display: Graph_Display.Graph =
    1.45      Graph_Display.make_graph(entries_graph)
    1.46  
     2.1 --- a/src/Pure/General/graph.ML	Tue Oct 10 17:15:37 2017 +0100
     2.2 +++ b/src/Pure/General/graph.ML	Tue Oct 10 19:51:54 2017 +0200
     2.3 @@ -40,6 +40,7 @@
     2.4    val maximals: 'a T -> key list
     2.5    val is_minimal: 'a T -> key -> bool
     2.6    val is_maximal: 'a T -> key -> bool
     2.7 +  val is_isolated: 'a T -> key -> bool
     2.8    val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
     2.9    val default_node: key * 'a -> 'a T -> 'a T
    2.10    val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
    2.11 @@ -177,6 +178,8 @@
    2.12  fun is_minimal G x = Keys.is_empty (imm_preds G x);
    2.13  fun is_maximal G x = Keys.is_empty (imm_succs G x);
    2.14  
    2.15 +fun is_isolated G x = is_minimal G x andalso is_maximal G x;
    2.16 +
    2.17  
    2.18  (* node operations *)
    2.19  
     3.1 --- a/src/Pure/General/graph.scala	Tue Oct 10 17:15:37 2017 +0100
     3.2 +++ b/src/Pure/General/graph.scala	Tue Oct 10 19:51:54 2017 +0200
     3.3 @@ -147,6 +147,8 @@
     3.4    def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
     3.5    def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
     3.6  
     3.7 +  def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
     3.8 +
     3.9  
    3.10    /* node operations */
    3.11  
     4.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 10 17:15:37 2017 +0100
     4.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 10 19:51:54 2017 +0200
     4.3 @@ -267,8 +267,7 @@
     4.4                }
     4.5  
     4.6                val imports_subgraph =
     4.7 -                sessions.imports_graph.restrict(
     4.8 -                  sessions.imports_graph.all_preds(info.parent.toList ::: info.imports).toSet)
     4.9 +                sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
    4.10  
    4.11                val graph0 =
    4.12                  (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
    4.13 @@ -356,7 +355,7 @@
    4.14    sealed case class Info(
    4.15      name: String,
    4.16      chapter: String,
    4.17 -    select: Boolean,
    4.18 +    dir_selected: Boolean,
    4.19      pos: Position.T,
    4.20      groups: List[String],
    4.21      dir: Path,
    4.22 @@ -369,6 +368,8 @@
    4.23      document_files: List[(Path, Path)],
    4.24      meta_digest: SHA1.Digest)
    4.25    {
    4.26 +    def deps: List[String] = parent.toList ::: imports
    4.27 +
    4.28      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    4.29    }
    4.30  
    4.31 @@ -424,7 +425,7 @@
    4.32            val select = sessions.toSet ++ graph.all_succs(base_sessions)
    4.33            (for {
    4.34              (name, (info, _)) <- graph.iterator
    4.35 -            if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
    4.36 +            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
    4.37            } yield name).toList
    4.38          }
    4.39        }.filterNot(excluded)