| Tue, 27 Aug 2013 12:35:32 +0200 |
wenzelm |
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 17:41:57 +0200 |
wenzelm |
strict checking of coordinates wrt. inner painter component;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:15:31 +0200 |
wenzelm |
more general window_geometry;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 13:18:26 +0200 |
wenzelm |
attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 23:57:29 +0200 |
wenzelm |
query process animation;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 22:54:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 29 Jun 2013 16:53:19 +0200 |
wenzelm |
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 10:37:38 +0100 |
wenzelm |
tuned signature;
|
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
|
| Wed, 06 Feb 2013 21:05:06 +0100 |
wenzelm |
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 19:53:24 +0100 |
wenzelm |
more uniform Pretty.char_width;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 21:01:00 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 18:44:27 +0100 |
wenzelm |
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 21:07:52 +0100 |
wenzelm |
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 12:22:55 +0100 |
wenzelm |
tuned signature in accordance to document operations;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 19:01:08 +0100 |
wenzelm |
prefer buffer_edit combinator over Java-style boilerplate;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 16:24:39 +0100 |
wenzelm |
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 14:24:30 +0100 |
wenzelm |
more accurate pixel_range -- do not round offset here;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 13:52:54 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 21:52:45 +0200 |
wenzelm |
more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 23:38:48 +0200 |
wenzelm |
further refinement of jEdit line range, avoiding lack of final \n;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 14:32:56 +0200 |
wenzelm |
further support for nested tooltips;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 13:48:22 +0200 |
wenzelm |
refer to parent frame -- relevant for floating dockables in particular;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 18:14:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 18:06:34 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 17:56:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 17:49:11 +0200 |
wenzelm |
somewhat more general JEdit_Lib;
|
file |
diff |
annotate
|