src/Tools/jEdit/src/completion_popup.scala
2014-02-25 wenzelm 2014-02-25 more completion rendering: active, semantic, syntactic; tuned;
2014-02-24 wenzelm 2014-02-24 tuned signature -- weaker type requirement;
2014-02-24 wenzelm 2014-02-24 paint completion range of active popup;
2014-02-23 wenzelm 2014-02-23 try explicit semantic completion before syntax completion;
2014-02-23 wenzelm 2014-02-23 more explicit Completion.Item.range, independently of caret;
2014-02-23 wenzelm 2014-02-23 clarified stretch_point_range wrt. UTF-16 surrogates; tuned;
2014-02-22 wenzelm 2014-02-22 refined language context: antiquotes; support default completions, with move of caret position; tuned signature;
2014-02-20 wenzelm 2014-02-20 default completion context via outer syntax; no symbol completion for ML files; tuned;
2014-02-20 wenzelm 2014-02-20 completion of keywords and symbols based on language context;
2013-11-08 wenzelm 2013-11-08 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
2013-11-08 wenzelm 2013-11-08 transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
2013-09-29 wenzelm 2013-09-29 explicit caret position after replacement;
2013-09-24 wenzelm 2013-09-24 clarified font;
2013-09-24 wenzelm 2013-09-24 disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
2013-09-22 wenzelm 2013-09-22 completion popup for history text field; imitate view font, for default rendering of symbols; tuned signature;
2013-09-04 wenzelm 2013-09-04 tuned;
2013-09-04 wenzelm 2013-09-04 interpret keys more movement only when needed;
2013-09-04 wenzelm 2013-09-04 remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); handle KP_UP/KP_DOWN keys as well, like Swing does;
2013-09-04 wenzelm 2013-09-04 no completion on backspace -- too intrusive, e.g. when deleting keywords;
2013-08-30 wenzelm 2013-08-30 sort items according to persistent history of frequency of use;
2013-08-30 wenzelm 2013-08-30 more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
2013-08-30 wenzelm 2013-08-30 allow short words for explicit completion;
2013-08-29 wenzelm 2013-08-29 border as for Pretty_Tooltip;
2013-08-29 wenzelm 2013-08-29 less aggressive immediate completion, based on input and text;
2013-08-29 wenzelm 2013-08-29 added action isabelle.complete, using standard jEdit keyboard shortcut;
2013-08-29 wenzelm 2013-08-29 option to insert unique completion immediately into buffer;
2013-08-29 wenzelm 2013-08-29 tuned signature;
2013-08-29 wenzelm 2013-08-29 maintain Completion_Popup.Text_Area as client property like Document_View; global Completion_Popup.Text_Area init/exit like SideKickPlugin; eliminated old SideKick completion -- cover all Isabelle modes uniformly; dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages;
2013-08-29 wenzelm 2013-08-29 some completion options;
2013-08-29 wenzelm 2013-08-29 more abstract Completion_Popup.Text_Area; more uniform font size;
2013-08-28 wenzelm 2013-08-28 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-28 wenzelm 2013-08-28 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); observe !evt.isConsumed semantically: no initial dismiss here (e.g. due to cursor keys);
2013-08-28 wenzelm 2013-08-28 dismiss popups more uniformly;
2013-08-28 wenzelm 2013-08-28 more uniform check (see JEdit_Lib.propagate_key);
2013-08-28 wenzelm 2013-08-28 tuned signature;
2013-08-27 wenzelm 2013-08-27 enable jEdit KeyEventWorkaround uniformly;
2013-08-27 wenzelm 2013-08-27 de-register completion first, which is important to make new popup reliably;
2013-08-27 wenzelm 2013-08-27 register single instance within root, in order to get rid of old popup as user continues typing;
2013-08-27 wenzelm 2013-08-27 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 wenzelm 2013-08-27 some actual completion via outer syntax; disable old SideKick completion for "isabelle" mode;
2013-08-27 wenzelm 2013-08-27 tuned signature;
2013-08-27 wenzelm 2013-08-27 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus; uniform JEdit_Lib.propagate_key;
2013-08-27 wenzelm 2013-08-27 determine completion geometry like tooltip; just one option jedit_popup_bounds for tooltip and completion;
2013-08-27 wenzelm 2013-08-27 explicit "hidden" operation with focus management; explicit popup_font; just one option jedit_popup_font_scale for tooltip and completion;
2013-08-27 wenzelm 2013-08-27 some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
2013-08-27 wenzelm 2013-08-27 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
2013-08-13 wenzelm 2013-08-13 Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);