# HG changeset patch
# User wenzelm
# Date 1583097251 -3600
# Node ID 248402f42cace49466139ed41842d1dcb562d769
# Parent  a3ed1b0a132f9a4d9b729eb1ee618ae8cdcc9756
clarified modifier: avoid confusion of CS+a as C+a;

diff -r a3ed1b0a132f -r 248402f42cac src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Mar 01 22:05:47 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Mar 01 22:14:11 2020 +0100
@@ -11,7 +11,7 @@
 import isabelle._
 
 import java.awt.{Color, Font, Toolkit, Window}
-import java.awt.event.KeyEvent
+import java.awt.event.{InputEvent, KeyEvent}
 import java.awt.im.InputMethodRequests
 import javax.swing.JTextField
 import javax.swing.event.{DocumentListener, DocumentEvent}
@@ -240,15 +240,21 @@
   addKeyListener(JEdit_Lib.key_listener(
     key_pressed = (evt: KeyEvent) =>
       {
+        val strict_control =
+        {
+          val mod = evt.getModifiersEx
+          (mod & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 &&
+          (mod & InputEvent.SHIFT_DOWN_MASK) == 0
+        }
+
         evt.getKeyCode match {
           case KeyEvent.VK_C | KeyEvent.VK_INSERT
-          if (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 &&
-              text_area.getSelectionCount != 0 =>
+          if strict_control && text_area.getSelectionCount != 0 =>
             Registers.copy(text_area, '$')
             evt.consume
 
           case KeyEvent.VK_A
-          if (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 =>
+          if strict_control =>
             text_area.selectAll
             evt.consume