# HG changeset patch
# User wenzelm
# Date 1396122110 -3600
# Node ID e925118b187566e4176a6f02856d4753a0dd0f34
# Parent  f9ad26836516987c4a1059a980b6d422662c0e6b
do not absorb vacuous copy operation, e.g. relevant when tooltip has focus but no selection, while the main text area has a selection but no focus;

diff -r f9ad26836516 -r e925118b1875 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 29 20:22:38 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 29 20:41:50 2014 +0100
@@ -166,7 +166,8 @@
       {
         evt.getKeyCode match {
           case KeyEvent.VK_C
-          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
+          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
+              text_area.getSelectionCount != 0 =>
             Registers.copy(text_area, '$')
             evt.consume