ignore isolated nodes by default;
authorwenzelm
Tue Oct 10 20:33:29 2017 +0200 (19 months ago)
changeset 66834c925393ae6b9
parent 66833 091012ac3dc2
child 66835 ecc99a5a1ab8
ignore isolated nodes by default;
src/Pure/General/graph_display.scala
     1.1 --- a/src/Pure/General/graph_display.scala	Tue Oct 10 19:51:54 2017 +0200
     1.2 +++ b/src/Pure/General/graph_display.scala	Tue Oct 10 20:33:29 2017 +0200
     1.3 @@ -63,10 +63,12 @@
     1.4  
     1.5    def make_graph[A](
     1.6      graph: isabelle.Graph[String, A],
     1.7 +    isolated: Boolean = false,
     1.8      name: (String, A) => String = (x: String, a: A) => x): Graph =
     1.9    {
    1.10      val entries =
    1.11 -      (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList
    1.12 +      (for { (x, (a, (ps, _))) <- graph.iterator if isolated || !graph.is_isolated(x) }
    1.13 +       yield ((x, (name(x, a), Nil)), ps.toList)).toList
    1.14      build_graph(entries)
    1.15    }
    1.16  }