tuned signature;

--- a/src/Tools/jEdit/src/document_view.scala	Sat Aug 24 14:58:36 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Aug 24 15:30:50 2013 +0200
@@ -72,7 +72,7 @@
 
   val rich_text_area =
     new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
-      caret_visible = true, hovering = false)
+      caret_visible = true, enable_hovering = false)
 
 
   /* perspective */

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Aug 24 14:58:36 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Aug 24 15:30:50 2013 +0200
@@ -72,7 +72,7 @@
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
-      caret_visible = false, hovering = true)
+      caret_visible = false, enable_hovering = true)
 
   def get_background(): Option[Color] = None
 

--- 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()