# HG changeset patch
# User wenzelm
# Date 1377358758 -7200
# Node ID 61b983193dc111bfeb339a1040d292c828417bd3
# Parent  7bf637b65ba27c0fe05cba5d83288bae570b1251
more static values;

diff -r 7bf637b65ba2 -r 61b983193dc1 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 16:06:15 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 17:39:18 2013 +0200
@@ -169,13 +169,15 @@
   }
 
   private val mouse_motion_listener = new MouseMotionAdapter {
-    override def mouseMoved(e: MouseEvent) {
+    override def mouseMoved(evt: MouseEvent) {
       robust_body(()) {
-        val control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
+        val x = evt.getX
+        val y = evt.getY
+        val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
 
         if ((control || enable_hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {
-            JEdit_Lib.pixel_range(text_area, e.getX, e.getY) match {
+            JEdit_Lib.pixel_range(text_area, x, y) match {
               case None => active_reset()
               case Some(range) =>
                 val rendering = get_rendering()
@@ -190,14 +192,12 @@
         }
         else active_reset()
 
-        if (e.getSource == text_area.getPainter) {
+        if (evt.getSource == text_area.getPainter) {
           Pretty_Tooltip.invoke(() =>
             robust_body(()) {
               val rendering = get_rendering()
               val snapshot = rendering.snapshot
               if (!snapshot.is_outdated) {
-                val x = e.getX
-                val y = e.getY
                 JEdit_Lib.pixel_range(text_area, x, y) match {
                   case None =>
                   case Some(range) =>
@@ -208,7 +208,7 @@
                       case None =>
                       case Some(tip) =>
                         val painter = text_area.getPainter
-                        val screen_point = e.getLocationOnScreen
+                        val screen_point = evt.getLocationOnScreen
                         screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
                         val results = rendering.command_results(range)
                         Pretty_Tooltip(view, painter, rendering, screen_point, results, tip)