clarified static full_graph vs. dynamic visible_graph;
tuned;

--- a/src/Pure/General/graph.scala	Sun Jan 04 13:34:42 2015 +0100
+++ b/src/Pure/General/graph.scala	Sun Jan 04 14:05:24 2015 +0100
@@ -181,6 +181,9 @@
 
   /* edge operations */
 
+  def edges_iterator: Iterator[(Key, Key)] =
+    for { x <- keys_iterator; y <- imm_succs(x).iterator } yield (x, y)
+
   def is_edge(x: Key, y: Key): Boolean =
     defined(x) && defined(y) && imm_succs(x)(y)
 

--- a/src/Tools/Graphview/graph_panel.scala	Sun Jan 04 13:34:42 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sun Jan 04 14:05:24 2015 +0100
@@ -27,9 +27,9 @@
 
   override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
     override def getToolTipText(event: java.awt.event.MouseEvent): String =
-      find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+      find_visible_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
         case Some(node) =>
-          visualizer.model.complete_graph.get_node(node) match {
+          visualizer.model.full_graph.get_node(node) match {
             case Nil => null
             case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content)
           }
@@ -45,10 +45,10 @@
 
   peer.getVerticalScrollBar.setUnitIncrement(10)
 
-  def find_node(at: Point2D): Option[Graph_Display.Node] =
+  def find_visible_node(at: Point2D): Option[Graph_Display.Node] =
   {
     val m = visualizer.metrics()
-    visualizer.model.visible_nodes_iterator
+    visualizer.model.make_visible_graph().keys_iterator
       .find(node => visualizer.Drawer.shape(m, node).contains(at))
   }
 
@@ -144,7 +144,7 @@
 
     def fit_to_window()
     {
-      if (visualizer.model.visible_nodes_iterator.isEmpty)
+      if (visualizer.model.make_visible_graph().is_empty)
         rescale(1.0)
       else {
         val box = visualizer.Coordinates.bounding_box()
@@ -181,7 +181,7 @@
     def dummy(at: Point2D): Option[Dummy] =
     {
       val m = visualizer.metrics()
-      visualizer.model.visible_edges_iterator.map(
+      visualizer.model.make_visible_graph().edges_iterator.map(
         edge => visualizer.Coordinates(edge).zipWithIndex.map((edge, _))).flatten.find(
           {
             case (_, ((x, y), _)) =>
@@ -197,7 +197,7 @@
     {
       val c = Transform.pane_to_graph_coordinates(at)
       val l =
-        find_node(c) match {
+        find_visible_node(c) match {
           case Some(node) =>
             if (visualizer.Selection.contains(node)) visualizer.Selection.get()
             else List(node)
@@ -221,7 +221,7 @@
 
       def left_click()
       {
-        (find_node(c), m) match {
+        (find_visible_node(c), m) match {
           case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
           case (None, Key.Modifier.Control) =>
 
@@ -238,7 +238,7 @@
 
       def right_click()
       {
-        val menu = Popups(panel, find_node(c), visualizer.Selection.get())
+        val menu = Popups(panel, find_visible_node(c), visualizer.Selection.get())
         menu.show(panel.peer, at.x, at.y)
       }
 

--- a/src/Tools/Graphview/model.scala	Sun Jan 04 13:34:42 2015 +0100
+++ b/src/Tools/Graphview/model.scala	Sun Jan 04 14:05:24 2015 +0100
@@ -33,7 +33,7 @@
 }
 
 
-class Model(val complete_graph: Graph_Display.Graph)
+class Model(val full_graph: Graph_Display.Graph)
 {
   val Mutators =
     new Mutator_Container(
@@ -51,16 +51,11 @@
         Mutator.Node_List(Nil, false, false, false)))
 
   def find_node(ident: String): Option[Graph_Display.Node] =
-    complete_graph.keys_iterator.find(node => node.ident == ident)
-
-  def visible_nodes_iterator: Iterator[Graph_Display.Node] = current_graph.keys_iterator
+    full_graph.keys_iterator.find(node => node.ident == ident)
 
-  def visible_edges_iterator: Iterator[Graph_Display.Edge] =
-    current_graph.keys_iterator.flatMap(k => current_graph.imm_succs(k).iterator.map((k, _)))
-
-  def current_graph: Graph_Display.Graph =
-    (complete_graph /: Mutators()) {
-      case (g, m) => if (!m.enabled) g else m.mutator.mutate(complete_graph, g)
+  def make_visible_graph(): Graph_Display.Graph =
+    (full_graph /: Mutators()) {
+      case (g, m) => if (!m.enabled) g else m.mutator.mutate(full_graph, g)
     }
 
   private var _colors = Map.empty[Graph_Display.Node, Color]
@@ -71,7 +66,7 @@
     _colors =
       (Map.empty[Graph_Display.Node, Color] /: Colors()) {
         case (colors, m) =>
-          (colors /: m.mutator.mutate(complete_graph, complete_graph).keys_iterator) {
+          (colors /: m.mutator.mutate(full_graph, full_graph).keys_iterator) {
             case (colors, node) => colors + (node -> m.color)
           }
       }

--- a/src/Tools/Graphview/mutator.scala	Sun Jan 04 13:34:42 2015 +0100
+++ b/src/Tools/Graphview/mutator.scala	Sun Jan 04 14:05:24 2015 +0100
@@ -34,8 +34,8 @@
     val description: String,
     pred: (Graph_Display.Graph, Graph_Display.Graph) => Graph_Display.Graph) extends Mutator
   {
-    def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph =
-      pred(complete_graph, graph)
+    def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph =
+      pred(full_graph, graph)
   }
 
   class Node_Filter(
@@ -144,20 +144,20 @@
       "Add by name",
       "Adds every node whose name matches the regex. " +
       "Adds all relevant edges.",
-      (complete_graph, graph) =>
-        add_node_group(complete_graph, graph,
-          complete_graph.keys.filter(node => (regex.r findFirstIn node.toString).isDefined).toList))
+      (full_graph, graph) =>
+        add_node_group(full_graph, graph,
+          full_graph.keys.filter(node => (regex.r findFirstIn node.toString).isDefined).toList))
 
   case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
     extends Graph_Mutator(
       "Add transitive closure",
       "Adds all family members of all current nodes.",
-      (complete_graph, graph) => {
+      (full_graph, graph) => {
         val withparents =
-          if (parents) add_node_group(complete_graph, graph, complete_graph.all_preds(graph.keys))
+          if (parents) add_node_group(full_graph, graph, full_graph.all_preds(graph.keys))
           else graph
         if (children)
-          add_node_group(complete_graph, withparents, complete_graph.all_succs(graph.keys))
+          add_node_group(full_graph, withparents, full_graph.all_succs(graph.keys))
         else withparents
       })
 }
@@ -166,13 +166,13 @@
 {
   val name: String
   val description: String
-  def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph
+  def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph
 
   override def toString: String = name
 }
 
 trait Filter extends Mutator
 {
-  def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph)
+  def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph)
   def filter(graph: Graph_Display.Graph): Graph_Display.Graph
 }

--- a/src/Tools/Graphview/popups.scala	Sun Jan 04 13:34:42 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Sun Jan 04 14:05:24 2015 +0100
@@ -24,7 +24,7 @@
     val visualizer = panel.visualizer
 
     val add_mutator = visualizer.model.Mutators.add _
-    val current_graph = visualizer.model.current_graph
+    val visible_graph = visualizer.model.make_visible_graph()
 
     def filter_context(
         nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =
@@ -57,7 +57,7 @@
           def degree_nodes(succs: Boolean) =
             (for {
               from <- nodes.iterator
-              tos = if (succs) current_graph.imm_succs(from) else current_graph.imm_preds(from)
+              tos = if (succs) visible_graph.imm_succs(from) else visible_graph.imm_preds(from)
               if tos.nonEmpty
             } yield (from, tos)).toList.sortBy(_._1)(Graph_Display.Node.Ordering)
 

--- a/src/Tools/Graphview/visualizer.scala	Sun Jan 04 13:34:42 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sun Jan 04 14:05:24 2015 +0100
@@ -146,15 +146,15 @@
     def update_layout()
     {
       val m = metrics()
+      val visible_graph = model.make_visible_graph()
 
       val max_width =
-        model.current_graph.keys_iterator.map(
-          node => m.string_bounds(node.toString).getWidth).max
+        visible_graph.keys_iterator.map(node => m.string_bounds(node.toString).getWidth).max
       val box_distance = (max_width + m.pad + m.gap).ceil
       def box_height(n: Int): Double = (m.char_width * 1.5 * (5 max n)).ceil
 
       // FIXME avoid expensive operation on GUI thread
-      layout = Layout.make(model.current_graph, box_distance, box_height _)
+      layout = Layout.make(visible_graph, box_distance, box_height _)
     }
 
     def bounding_box(): Rectangle2D.Double =
@@ -164,7 +164,7 @@
       var y0 = 0.0
       var x1 = 0.0
       var y1 = 0.0
-      for (node <- model.visible_nodes_iterator) {
+      for (node <- model.make_visible_graph().keys_iterator) {
         val shape = Shapes.Node.shape(m, visualizer, node)
         x0 = x0 min shape.getMinX
         y0 = y0 min shape.getMinY
@@ -189,10 +189,11 @@
 
     def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
     {
-      gfx.setFont(font)
+      gfx.setFont(font())
       gfx.setRenderingHints(rendering_hints)
-      model.visible_edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
-      model.visible_nodes_iterator.foreach(apply(gfx, _))
+      val visible_graph = model.make_visible_graph()
+      visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
+      visible_graph.keys_iterator.foreach(apply(gfx, _))
     }
 
     def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =