# HG changeset patch
# User wenzelm
# Date 1583096747 -3600
# Node ID a3ed1b0a132f9a4d9b729eb1ee618ae8cdcc9756
# Parent  29f37eb9bd0fa96b82ab0679915aca578695f2ce
tuned -- avoid deprecated operations;

diff -r 29f37eb9bd0f -r a3ed1b0a132f src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Mar 01 21:52:21 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Mar 01 22:05:47 2020 +0100
@@ -388,10 +388,10 @@
   def special_key(evt: KeyEvent): Boolean =
   {
     // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
-    val mod = evt.getModifiers
-    (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
-    (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
+    val mod = evt.getModifiersEx
+    (mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 ||
+    (mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 &&
       !Debug.ALT_KEY_PRESSED_DISABLED ||
-    (mod & InputEvent.META_MASK) != 0
+    (mod & InputEvent.META_DOWN_MASK) != 0
   }
 }
diff -r 29f37eb9bd0f -r a3ed1b0a132f src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Mar 01 21:52:21 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Mar 01 22:05:47 2020 +0100
@@ -242,13 +242,13 @@
       {
         evt.getKeyCode match {
           case KeyEvent.VK_C | KeyEvent.VK_INSERT
-          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
+          if (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 &&
               text_area.getSelectionCount != 0 =>
             Registers.copy(text_area, '$')
             evt.consume
 
           case KeyEvent.VK_A
-          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
+          if (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 =>
             text_area.selectAll
             evt.consume