src/Tools/jEdit/src/completion_popup.scala
2013-08-30 ago more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
2013-08-30 ago allow short words for explicit completion;
2013-08-29 ago border as for Pretty_Tooltip;
2013-08-29 ago less aggressive immediate completion, based on input and text;
2013-08-29 ago added action isabelle.complete, using standard jEdit keyboard shortcut;
2013-08-29 ago option to insert unique completion immediately into buffer;
2013-08-29 ago tuned signature;
2013-08-29 ago maintain Completion_Popup.Text_Area as client property like Document_View;
2013-08-29 ago some completion options;
2013-08-29 ago more abstract Completion_Popup.Text_Area;
2013-08-28 ago uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-28 ago more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
2013-08-28 ago dismiss popups more uniformly;
2013-08-28 ago more uniform check (see JEdit_Lib.propagate_key);
2013-08-28 ago tuned signature;
2013-08-27 ago enable jEdit KeyEventWorkaround uniformly;
2013-08-27 ago de-register completion first, which is important to make new popup reliably;
2013-08-27 ago register single instance within root, in order to get rid of old popup as user continues typing;
2013-08-27 ago more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
2013-08-27 ago some actual completion via outer syntax;
2013-08-27 ago tuned signature;
2013-08-27 ago avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
2013-08-27 ago determine completion geometry like tooltip;
2013-08-27 ago explicit "hidden" operation with focus management;
2013-08-27 ago some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
2013-08-27 ago more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
2013-08-13 ago Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);