| Sun, 13 Apr 2014 21:43:25 +0200 |
wenzelm |
added spell-checker completion dialog, without counting frequency of items due to empty name;
|
file |
diff |
annotate
|
| Sun, 13 Apr 2014 19:55:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 13 Apr 2014 19:18:30 +0200 |
wenzelm |
tuned rendering -- avoid overlap with squiggly underline;
|
file |
diff |
annotate
|
| Sun, 13 Apr 2014 16:06:55 +0200 |
wenzelm |
tuned signature -- explicit Spell_Checker_Variable;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 21:00:04 +0200 |
wenzelm |
more general spell_checker_elements;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 20:49:57 +0200 |
wenzelm |
added spell-checker options;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 16:22:06 +0200 |
wenzelm |
dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 15:19:22 +0200 |
wenzelm |
clarifed results range;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 13:32:34 +0200 |
wenzelm |
avoid confusion about pointless cursor movement with external links;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 14:30:26 +0200 |
wenzelm |
prepare "back" position for Navigator, before following hyperlink;
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 14:31:31 +0200 |
wenzelm |
revert ce37fcb30cf2 for the sake of Mac OS X -- let some event listeners of jEdit reset the cursor;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 20:41:44 +0200 |
wenzelm |
tuned signature -- more explicit iterator terminology;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 11:55:37 +0200 |
wenzelm |
more uniform painting of caret, which also improves visibility in invisible state;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 20:07:59 +0200 |
wenzelm |
clear active areas (notably mouse pointer) before changing context (e.g. via hyperlink);
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 18:28:35 +0200 |
wenzelm |
reset mouse pointer more decisively, for the sake of Mac OS X (despite the builtin policie of jEdit);
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 20:22:38 +0100 |
wenzelm |
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 12:42:24 +0100 |
wenzelm |
dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2014 11:29:42 +0100 |
wenzelm |
tuned rendering -- change mouse pointer for active areas;
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 11:39:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 17:56:59 +0100 |
wenzelm |
simplified rendering -- no need to over-emphasize "token_range";
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 12:15:49 +0100 |
wenzelm |
improved rendering of blinking cursor;
|
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 19:33:39 +0100 |
wenzelm |
tuned colors;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 12:51:55 +0100 |
wenzelm |
clarified painting of invisible caret, e.g. focus change due to popup;
|
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 16:08:38 +0100 |
wenzelm |
clarified stretch_point_range wrt. UTF-16 surrogates;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 15:35:19 +0100 |
wenzelm |
some rendering of completion range;
|
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
|
| Sat, 24 Aug 2013 17:39:18 +0200 |
wenzelm |
more static values;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 15:34:09 +0200 |
wenzelm |
prefer static "control", which is determined when the mouse event happens, not when its action runs;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 15:30:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 17:11:27 +0200 |
wenzelm |
manage hyperlinks via PIDE editor interface;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 21:23:06 +0200 |
wenzelm |
more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:04:46 +0200 |
wenzelm |
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
|
file |
diff |
annotate
|
| Mon, 01 Jul 2013 14:56:10 +0200 |
wenzelm |
avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
|
file |
diff |
annotate
|
| Mon, 01 Jul 2013 14:37:31 +0200 |
wenzelm |
more robust delayed invocation;
|
file |
diff |
annotate
|
| Mon, 01 Jul 2013 14:30:56 +0200 |
wenzelm |
clarified tooltip timing of pending event and active state;
|
file |
diff |
annotate
|
| Sat, 29 Jun 2013 21:28:24 +0200 |
wenzelm |
more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
|
file |
diff |
annotate
|
| Sat, 29 Jun 2013 20:40:08 +0200 |
wenzelm |
explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
|
file |
diff |
annotate
|
| Sat, 29 Jun 2013 18:20:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 22:26:25 +0100 |
wenzelm |
paint bullet bar within text layer -- thus it remains visible with active selection etc.;
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 13:32:53 +0100 |
wenzelm |
improved centering via strikethrough offset;
|
file |
diff |
annotate
|
| Thu, 28 Mar 2013 22:42:18 +0100 |
wenzelm |
ghost bullet via markup, which is painted as bar under text (normally space);
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 19:39:31 +0100 |
wenzelm |
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 13:12:39 +0100 |
wenzelm |
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
|
file |
diff |
annotate
|
| Thu, 21 Mar 2013 16:35:53 +0100 |
wenzelm |
eliminated char_width_int to avoid unclear rounding;
|
file |
diff |
annotate
|
| Mon, 18 Mar 2013 11:29:50 +0100 |
wenzelm |
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
|
file |
diff |
annotate
|
| Sun, 17 Mar 2013 21:04:38 +0100 |
wenzelm |
explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
|
file |
diff |
annotate
|
| Sat, 16 Mar 2013 21:26:44 +0100 |
wenzelm |
more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 21:09:29 +0100 |
wenzelm |
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 19:53:24 +0100 |
wenzelm |
more uniform Pretty.char_width;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 20:30:03 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 18:23:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 20:05:53 +0100 |
wenzelm |
prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:46:33 +0100 |
wenzelm |
include command results in tooltip as well;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Sat, 01 Dec 2012 19:51:43 +0100 |
wenzelm |
updated to jedit-5.0.0;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:22:29 +0100 |
wenzelm |
reset active areas on content update;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
file |
diff |
annotate
|