# HG changeset patch
# User wenzelm
# Date 1507660409 -7200
# Node ID c925393ae6b93f2f2fdd83135db84676e2b45423
# Parent  091012ac3dc27a83b4fa08ed1f2171af5c1ea8c4
ignore isolated nodes by default;

diff -r 091012ac3dc2 -r c925393ae6b9 src/Pure/General/graph_display.scala
--- a/src/Pure/General/graph_display.scala	Tue Oct 10 19:51:54 2017 +0200
+++ b/src/Pure/General/graph_display.scala	Tue Oct 10 20:33:29 2017 +0200
@@ -63,10 +63,12 @@
 
   def make_graph[A](
     graph: isabelle.Graph[String, A],
+    isolated: Boolean = false,
     name: (String, A) => String = (x: String, a: A) => x): Graph =
   {
     val entries =
-      (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList
+      (for { (x, (a, (ps, _))) <- graph.iterator if isolated || !graph.is_isolated(x) }
+       yield ((x, (name(x, a), Nil)), ps.toList)).toList
     build_graph(entries)
   }
 }