src/Tools/jEdit/src/rich_text_area.scala

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 14:58:36 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 15:30:50 2013 +0200
@@ -29,7 +29,7 @@
   get_rendering: () => Rendering,
   close_action: () => Unit,
   caret_visible: Boolean,
-  hovering: Boolean)
+  enable_hovering: Boolean)
 {
   private val buffer = text_area.getBuffer
 
@@ -175,7 +175,7 @@
       robust_body(()) {
         control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
 
-        if ((control || hovering) && !buffer.isLoading) {
+        if ((control || enable_hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {
             JEdit_Lib.pixel_range(text_area, e.getX, e.getY) match {
               case None => active_reset()