prefer static "control", which is determined when the mouse event happens, not when its action runs;

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 15:30:50 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 15:34:09 2013 +0200
@@ -132,8 +132,6 @@
 
   // owned by Swing thread
 
-  private var control: Boolean = false
-
   private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
   private val hyperlink_area =
     new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _)
@@ -173,7 +171,7 @@
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseMoved(e: MouseEvent) {
       robust_body(()) {
-        control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
+        val control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
 
         if ((control || enable_hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {