src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -12,7 +12,6 @@
 
 import java.awt.{Dimension, Graphics2D, Point}
 import java.awt.geom.{AffineTransform, Point2D}
-import java.awt.image.BufferedImage
 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
 
 import scala.swing.{Panel, ScrollPane}
@@ -46,11 +45,8 @@
   peer.getVerticalScrollBar.setUnitIncrement(10)
 
   def find_visible_node(at: Point2D): Option[Graph_Display.Node] =
-  {
-    val m = visualizer.metrics()
-    visualizer.model.make_visible_graph().keys_iterator
-      .find(node => visualizer.Drawer.shape(m, node).contains(at))
-  }
+    visualizer.visible_graph.keys_iterator.find(node =>
+      visualizer.Drawer.shape(node).contains(at))
 
   def refresh()
   {
@@ -133,7 +129,7 @@
 
     def scale_discrete: Double =
     {
-      val font_height = GUI.line_metrics(visualizer.font()).getHeight.toInt
+      val font_height = GUI.line_metrics(visualizer.metrics.font).getHeight.toInt
       (scale * font_height).floor / font_height
     }
 
@@ -147,7 +143,7 @@
 
     def fit_to_window()
     {
-      if (visualizer.model.make_visible_graph().is_empty)
+      if (visualizer.visible_graph.is_empty)
         rescale(1.0)
       else {
         val box = visualizer.Coordinates.bounding_box()
@@ -181,18 +177,16 @@
 
     def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] =
     {
-      val m = visualizer.metrics()
-      visualizer.model.make_visible_graph().edges_iterator.map(
-        edge =>
-          visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find(
-            {
-              case (_, (p, _)) =>
-                visualizer.Drawer.shape(m, Graph_Display.Node.dummy).
-                  contains(at.getX() - p.x, at.getY() - p.y)
-            }) match {
-              case None => None
-              case Some((edge, (_, index))) => Some((edge, index))
-            }
+      visualizer.visible_graph.edges_iterator.map(edge =>
+        visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find(
+          {
+            case (_, (p, _)) =>
+              visualizer.Drawer.shape(Graph_Display.Node.dummy).
+                contains(at.getX() - p.x, at.getY() - p.y)
+          }) match {
+            case None => None
+            case Some((edge, (_, index))) => Some((edge, index))
+          }
     }
 
     def pressed(at: Point)