src/Tools/jEdit/src/completion_popup.scala
Wed, 28 Aug 2013 09:12:50 +0200 wenzelm more uniform check (see JEdit_Lib.propagate_key);
Wed, 28 Aug 2013 09:08:36 +0200 wenzelm tuned signature;
Tue, 27 Aug 2013 22:23:40 +0200 wenzelm enable jEdit KeyEventWorkaround uniformly;
Tue, 27 Aug 2013 22:20:11 +0200 wenzelm de-register completion first, which is important to make new popup reliably;
Tue, 27 Aug 2013 22:00:35 +0200 wenzelm register single instance within root, in order to get rid of old popup as user continues typing;
Tue, 27 Aug 2013 20:58:53 +0200 wenzelm more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
Tue, 27 Aug 2013 20:45:02 +0200 wenzelm some actual completion via outer syntax;
Tue, 27 Aug 2013 17:17:20 +0200 wenzelm tuned signature;
Tue, 27 Aug 2013 16:45:32 +0200 wenzelm avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
Tue, 27 Aug 2013 16:09:28 +0200 wenzelm determine completion geometry like tooltip;
Tue, 27 Aug 2013 15:35:51 +0200 wenzelm explicit "hidden" operation with focus management;
Tue, 27 Aug 2013 14:56:11 +0200 wenzelm some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
Tue, 27 Aug 2013 12:35:32 +0200 wenzelm more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
Tue, 13 Aug 2013 22:25:24 +0200 wenzelm Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
less more (0) tip