# HG changeset patch
# User wenzelm
# Date 1420228454 -3600
# Node ID d20cdab3bfeb52ce205f8e50c4844d4bf1a20969
# Parent  8a85fe32c2787b661352e54b7934724ad8b808b2
less excessive event handling;

diff -r 8a85fe32c278 -r d20cdab3bfeb 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() }