# HG changeset patch
# User wenzelm
# Date 1377351249 -7200
# Node ID 04590977dc3cb9eece3bd15901a0f94b30a9da35
# Parent  336cd976698c76e00492b8384969127385731608
prefer static "control", which is determined when the mouse event happens, not when its action runs;

diff -r 336cd976698c -r 04590977dc3c src/Tools/jEdit/src/rich_text_area.scala
--- 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) {