equal
deleted
inserted
replaced
232 |
232 |
233 override def mouseMoved(evt: MouseEvent) { |
233 override def mouseMoved(evt: MouseEvent) { |
234 robust_body(()) { |
234 robust_body(()) { |
235 val x = evt.getX |
235 val x = evt.getX |
236 val y = evt.getY |
236 val y = evt.getY |
237 val control = (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 |
237 val control = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 |
238 |
238 |
239 if ((control || enable_hovering) && !buffer.isLoading) { |
239 if ((control || enable_hovering) && !buffer.isLoading) { |
240 JEdit_Lib.buffer_lock(buffer) { |
240 JEdit_Lib.buffer_lock(buffer) { |
241 JEdit_Lib.pixel_range(text_area, x, y) match { |
241 JEdit_Lib.pixel_range(text_area, x, y) match { |
242 case None => active_reset() |
242 case None => active_reset() |