| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 19:39:27 +0100 |
wenzelm |
tuned signature -- separate module Font_Info;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 22:19:29 +0100 |
wenzelm |
allow completion within a word (or symbol), like semantic completion;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 14:59:24 +0100 |
wenzelm |
more precise before_caret_range (looking both in space and time);
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 22:13:57 +0100 |
wenzelm |
uniform insert vs. popup policy;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 20:57:57 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 20:46:09 +0100 |
wenzelm |
no word completion within word context;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 20:15:47 +0100 |
wenzelm |
more completion rendering: active, semantic, syntactic;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 12:23:35 +0100 |
wenzelm |
tuned signature -- weaker type requirement;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 12:14:03 +0100 |
wenzelm |
paint completion range of active popup;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 20:24:33 +0100 |
wenzelm |
try explicit semantic completion before syntax completion;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 19:29:27 +0100 |
wenzelm |
more explicit Completion.Item.range, independently of caret;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 16:08:38 +0100 |
wenzelm |
clarified stretch_point_range wrt. UTF-16 surrogates;
|
file |
diff |
annotate
|
| Sat, 22 Feb 2014 15:07:33 +0100 |
wenzelm |
refined language context: antiquotes;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 13:23:49 +0100 |
wenzelm |
default completion context via outer syntax;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 12:53:12 +0100 |
wenzelm |
completion of keywords and symbols based on language context;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2013 17:34:37 +0100 |
wenzelm |
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
|
file |
diff |
annotate
|
| Fri, 08 Nov 2013 15:10:16 +0100 |
wenzelm |
transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
|
file |
diff |
annotate
|
| Sun, 29 Sep 2013 18:51:01 +0200 |
wenzelm |
explicit caret position after replacement;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 19:57:44 +0200 |
wenzelm |
clarified font;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 19:41:14 +0200 |
wenzelm |
disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
|
file |
diff |
annotate
|
| Sun, 22 Sep 2013 18:07:34 +0200 |
wenzelm |
completion popup for history text field;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 17:40:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 17:35:47 +0200 |
wenzelm |
interpret keys more movement only when needed;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 12:20:00 +0200 |
wenzelm |
remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 11:12:00 +0200 |
wenzelm |
no completion on backspace -- too intrusive, e.g. when deleting keywords;
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 23:38:18 +0200 |
wenzelm |
sort items according to persistent history of frequency of use;
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 13:24:14 +0200 |
wenzelm |
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 12:44:39 +0200 |
wenzelm |
allow short words for explicit completion;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 22:40:50 +0200 |
wenzelm |
border as for Pretty_Tooltip;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 22:35:50 +0200 |
wenzelm |
less aggressive immediate completion, based on input and text;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 21:49:46 +0200 |
wenzelm |
added action isabelle.complete, using standard jEdit keyboard shortcut;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 21:17:46 +0200 |
wenzelm |
option to insert unique completion immediately into buffer;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 13:00:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 12:38:33 +0200 |
wenzelm |
maintain Completion_Popup.Text_Area as client property like Document_View;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 10:24:43 +0200 |
wenzelm |
some completion options;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 10:01:59 +0200 |
wenzelm |
more abstract Completion_Popup.Text_Area;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 16:36:46 +0200 |
wenzelm |
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 15:14:58 +0200 |
wenzelm |
more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 09:36:05 +0200 |
wenzelm |
dismiss popups more uniformly;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 09:12:50 +0200 |
wenzelm |
more uniform check (see JEdit_Lib.propagate_key);
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 09:08:36 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 22:23:40 +0200 |
wenzelm |
enable jEdit KeyEventWorkaround uniformly;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 22:20:11 +0200 |
wenzelm |
de-register completion first, which is important to make new popup reliably;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 20:45:02 +0200 |
wenzelm |
some actual completion via outer syntax;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 17:17:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 16:09:28 +0200 |
wenzelm |
determine completion geometry like tooltip;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 15:35:51 +0200 |
wenzelm |
explicit "hidden" operation with focus management;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 14:56:11 +0200 |
wenzelm |
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 12:35:32 +0200 |
wenzelm |
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|