--- a/src/Tools/jEdit/src/jedit_lib.scala Sun Dec 13 14:58:14 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Dec 13 16:00:52 2020 +0100
@@ -10,7 +10,7 @@
import isabelle._
import java.io.{File => JFile}
-import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
+import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}
import java.awt.event.{InputEvent, KeyEvent, KeyListener}
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
@@ -394,4 +394,10 @@
!Debug.ALT_KEY_PRESSED_DISABLED ||
(mod & InputEvent.META_DOWN_MASK) != 0
}
+
+ def command_modifier(evt: InputEvent): Boolean =
+ (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0
+
+ def shift_modifier(evt: InputEvent): Boolean =
+ (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0
}