# HG changeset patch
# User wenzelm
# Date 1355598353 -3600
# Node ID ce0398b766ce8189da0a3b76f2e78cf293efcdd4
# Parent  2b7fd8c9c4acb607e3b4f7c4c60392a603873ae6
prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;

diff -r 2b7fd8c9c4ac -r ce0398b766ce src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Dec 15 18:30:09 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Dec 15 20:05:53 2012 +0100
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Window, Color, Point}
+import java.awt.{Graphics2D, Shape, Window, Color, Point, Toolkit}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import java.awt.font.TextAttribute
@@ -168,7 +168,7 @@
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseMoved(e: MouseEvent) {
       robust_body(()) {
-        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+        control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
 
         if ((control || hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {