ignore isolated nodes by default;

--- 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)
   }
 }