NEWS
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".