src/Tools/jEdit/src/rich_text_area.scala

   view: View,
   text_area: TextArea,
   get_rendering: () => Rendering,
   close_action: () => Unit,
   caret_visible: Boolean,
-  hovering: Boolean)
+  enable_hovering: Boolean)
 {
   private val buffer = text_area.getBuffer
 
 
   /* robust extension body */

   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseMoved(e: MouseEvent) {
       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()
               case Some(range) =>
                 val rendering = get_rendering()