src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Fri Jan 02 20:37:34 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Fri Jan 02 20:54:14 2015 +0100
@@ -15,8 +15,7 @@
 import javax.swing.{JScrollPane, JComponent, SwingUtilities}
 
 import scala.swing.{Panel, ScrollPane}
-import scala.swing.event.{Event, Key, KeyTyped, MousePressed, MouseDragged,
-  MouseMoved, MouseClicked, MouseEvent}
+import scala.swing.event.{Event, Key, KeyTyped, MousePressed, MouseDragged, MouseClicked, MouseEvent}
 
 
 class Graph_Panel(val visualizer: Visualizer) extends ScrollPane
@@ -114,7 +113,6 @@
     case MousePressed(_, _, _, _, _) => repaint(); requestFocus()
     case MouseDragged(_, _, _) => repaint(); requestFocus()
     case MouseClicked(_, _, _, _, _) => repaint(); requestFocus()
-    case MouseMoved(_, _, _) => repaint()
   }
 
   visualizer.model.Colors.events += { case _ => repaint() }