changeset 57833 | 2c2bae3da1c2 |
parent 57826 | a01caa7145d4 |
child 57856 | 73c683e09401 |
--- a/NEWS Thu Jul 31 20:59:10 2014 +0200 +++ b/NEWS Thu Jul 31 21:29:31 2014 +0200 @@ -85,6 +85,9 @@ handling and propagation to enclosing text area -- avoid loosing keystrokes with slow / remote graphics displays. +* Completion popup supports both ENTER and TAB (default) to select an +item, depending on Isabelle options. + * Refined insertion of completion items wrt. jEdit text: multiple selections, rectangular selections, rectangular selection as "tall caret".