Ticket #402: MouseMover_20071013.patch

src/org/openstreetmap/josm/gui/MapMover.java

@@ -92 +92 @@
         /**
          * If the right (and only the right) mouse button is pressed, move the map
          */
-        public void mouseDragged(MouseEvent e) {
+        @Override public void mouseDragged(MouseEvent e) {
                 int offMask = MouseEvent.BUTTON1_DOWN_MASK | MouseEvent.BUTTON2_DOWN_MASK;
                 if ((e.getModifiersEx() & (MouseEvent.BUTTON3_DOWN_MASK | offMask)) == MouseEvent.BUTTON3_DOWN_MASK) {
                         if (mousePosMove == null)
@@ -157 +157 @@
          * Zoom the map by 1/5th of current zoom per wheel-delta.
          * @param e The wheel event.
          */
-        public void mouseWheelMoved(MouseWheelEvent e) {
+        @Override public void mouseWheelMoved(MouseWheelEvent e) {
                 int w = nc.getWidth();
                 int h = nc.getHeight();
 
@@ -176 +176 @@
         /**
          * Does nothing. Only to satisfy MouseMotionListener
          */
-        public void mouseMoved(MouseEvent e) {}
+        @Override public void mouseMoved(MouseEvent e) {}
 }