Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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;
authorwenzelm
Sat, 29 Mar 2014 20:41:50 +0100
changeset 56323 e925118b1875
parent 56322 f9ad26836516
child 56324 f9de5e5b56e6
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;
src/Tools/jEdit/src/pretty_text_area.scala file | annotate | diff | comparison | revisions 
--- 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
isabelle