# HG changeset patch
# User wenzelm
# Date 1607871652 -3600
# Node ID 8732315dfafac0bceca1557400f8c3360918e211
# Parent  4e4b4298f1e7579b7830358c5ced21884f864253
tuned signature;

diff -r 4e4b4298f1e7 -r 8732315dfafa src/Tools/jEdit/src/jedit_lib.scala
--- 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
 }
diff -r 4e4b4298f1e7 -r 8732315dfafa src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Dec 13 14:58:14 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Dec 13 16:00:52 2020 +0100
@@ -205,11 +205,7 @@
     key_pressed = (evt: KeyEvent) =>
       {
         val strict_control =
-        {
-          val mod = evt.getModifiersEx
-          (mod & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 &&
-          (mod & InputEvent.SHIFT_DOWN_MASK) == 0
-        }
+          JEdit_Lib.command_modifier(evt) && !JEdit_Lib.shift_modifier(evt)
 
         evt.getKeyCode match {
           case KeyEvent.VK_C | KeyEvent.VK_INSERT
diff -r 4e4b4298f1e7 -r 8732315dfafa src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 13 14:58:14 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 13 16:00:52 2020 +0100
@@ -233,7 +233,7 @@
       robust_body(()) {
         val x = evt.getX
         val y = evt.getY
-        val control = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0
+        val control = JEdit_Lib.command_modifier(evt)
 
         if ((control || enable_hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {