src/Tools/Graphview/graph_panel.scala

       paint_panel.set_preferred_size()
       paint_panel.repaint()
     }
   }
 
-  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)
   {
     Transform.scale = s

 
   rescale(1.0)
 
 
   /* transform */
+
+  def fit_to_window()
+  {
+    Transform.fit_to_window()
+    refresh()
+  }
 
   private object Transform
   {
     private var _scale: Double = 1.0
     def scale: Double = _scale

     }
   }
 
 
   /* interaction */
+
+  visualizer.model.Colors.events += { case _ => repaint() }
+  visualizer.model.Mutators.events += { case _ => repaint() }
 
   listenTo(mouse.moves)
   listenTo(mouse.clicks)
   reactions +=
   {

     case e @ MouseClicked(_, p, m, n, _) =>
       Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer))
       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]) =
       (new Point(0, 0), Nil, Nil)