diff -r ea163bf8ad22 -r 47fb85ccfce8 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Sun Jan 18 22:03:53 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sun Jan 18 22:07:45 2015 +0100
@@ -100,12 +100,6 @@
     }
   }
 
-  def fit_to_window()
-  {
-    Transform.fit_to_window()
-    refresh()
-  }
-
   val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
 
   def rescale(s: Double)
@@ -120,6 +114,12 @@
 
   /* transform */
 
+  def fit_to_window()
+  {
+    Transform.fit_to_window()
+    refresh()
+  }
+
   private object Transform
   {
     private var _scale: Double = 1.0
@@ -166,6 +166,9 @@
 
   /* interaction */
 
+  visualizer.model.Colors.events += { case _ => repaint() }
+  visualizer.model.Mutators.events += { case _ => repaint() }
+
   listenTo(mouse.moves)
   listenTo(mouse.clicks)
   reactions +=
@@ -181,9 +184,6 @@
       repaint()
   }
 
-  visualizer.model.Colors.events += { case _ => repaint() }
-  visualizer.model.Mutators.events += { case _ => repaint() }
-
   private object Mouse_Interaction
   {
     private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) =