| 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:57:46 +0100 |
wenzelm |
allow fractional pretty margin -- avoid premature rounding;
|
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
|
| Mon, 18 Mar 2013 20:02:37 +0100 |
wenzelm |
prefer ownerless window, to avoid question of potentially changing parent view;
|
file |
diff |
annotate
|
| Mon, 18 Mar 2013 19:33:25 +0100 |
wenzelm |
proper parent component for window.init;
|
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
|
| Mon, 18 Mar 2013 11:04:59 +0100 |
wenzelm |
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
|
file |
diff |
annotate
|
| Sun, 17 Mar 2013 22:02:06 +0100 |
wenzelm |
re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
|
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 17:16:39 +0100 |
wenzelm |
some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;
|
file |
diff |
annotate
|
| Sat, 16 Mar 2013 12:46:22 +0100 |
wenzelm |
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
|
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
|
| Sat, 05 Jan 2013 20:06:24 +0100 |
wenzelm |
propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 17:37:29 +0100 |
wenzelm |
more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 21:41:22 +0100 |
wenzelm |
prefer JDialog over JWindow to avoid focus inversion problem on Compiz (e.g. Ubuntu/Unity 12.10): both JDialog and JFrame happen to work, but JFrame does not support parent nesting;
|
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
|
| Fri, 14 Dec 2012 21:26:01 +0100 |
wenzelm |
init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;
|
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
|
| Sun, 25 Nov 2012 21:10:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 18:47:33 +0100 |
wenzelm |
quasi-abstract module Rendering, with Isabelle-specific implementation;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 17:11:26 +0100 |
wenzelm |
pack window before accessing its geometry;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2012 16:55:53 +0100 |
wenzelm |
more precise tooltip window size;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 14:06:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 00:08:36 +0200 |
wenzelm |
improved adhoc height for small fonts;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 22:53:20 +0200 |
wenzelm |
more uniform tooltip color;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:40:35 +0200 |
wenzelm |
use Pretty_Tooltip for Graphview_Panel;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2012 16:26:31 +0200 |
wenzelm |
close tooltips more thoroughly;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2012 16:15:31 +0200 |
wenzelm |
make buttons closer to original mouse position;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2012 16:05:31 +0200 |
wenzelm |
detach tooltip as dockable window;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2012 15:05:11 +0200 |
wenzelm |
explicit close button;
|
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
|
| Fri, 05 Oct 2012 12:11:23 +0200 |
wenzelm |
tuned window position to fit on screen;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 12:00:28 +0200 |
wenzelm |
tuned window position;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 11:36:46 +0200 |
wenzelm |
determine window size from content;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 11:09:24 +0200 |
wenzelm |
tuned color and font size;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 10:54:07 +0200 |
wenzelm |
close tooltip window on escape;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 20:36:10 +0200 |
wenzelm |
some re-ordering of initialization to ensure proper formatting;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 20:14:40 +0200 |
wenzelm |
separate module Pretty_Tooltip;
|
file |
diff |
annotate
|