src/Tools/jEdit/src/pretty_tooltip.scala
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;
Sat, 23 Mar 2013 13:57:46 +0100 wenzelm allow fractional pretty margin -- avoid premature rounding;
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);
Mon, 18 Mar 2013 20:02:37 +0100 wenzelm prefer ownerless window, to avoid question of potentially changing parent view;
Mon, 18 Mar 2013 19:33:25 +0100 wenzelm proper parent component for window.init;
Mon, 18 Mar 2013 11:29:50 +0100 wenzelm extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
Mon, 18 Mar 2013 11:04:59 +0100 wenzelm recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
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;
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);
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;
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);
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);
Sat, 12 Jan 2013 19:53:24 +0100 wenzelm more uniform Pretty.char_width;
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;
Fri, 04 Jan 2013 17:37:29 +0100 wenzelm more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
less more (0) -15 tip