src/Tools/jEdit/src/pretty_tooltip.scala
2013-03-23 ago retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23 ago allow fractional pretty margin -- avoid premature rounding;
2013-03-23 ago 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);
2013-03-18 ago prefer ownerless window, to avoid question of potentially changing parent view;
2013-03-18 ago proper parent component for window.init;
2013-03-18 ago extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
2013-03-18 ago recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
2013-03-17 ago re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
2013-03-17 ago 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);
2013-03-16 ago some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;
2013-03-16 ago more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
2013-01-16 ago close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
2013-01-12 ago more uniform Pretty.char_width;
2013-01-05 ago propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
2013-01-04 ago more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
2012-12-31 ago 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;
2012-12-15 ago more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
2012-12-14 ago init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;
2012-12-13 ago more careful handling of Dialog_Result, with active area and color feedback;
2012-11-25 ago tuned signature;
2012-11-25 ago renamed main plugin object to PIDE;
2012-11-25 ago quasi-abstract module Rendering, with Isabelle-specific implementation;
2012-11-22 ago pack window before accessing its geometry;
2012-11-22 ago more precise tooltip window size;
2012-11-21 ago tuned;
2012-10-13 ago improved adhoc height for small fonts;
2012-10-12 ago more uniform tooltip color;
2012-10-08 ago use Pretty_Tooltip for Graphview_Panel;
2012-10-07 ago close tooltips more thoroughly;
2012-10-07 ago make buttons closer to original mouse position;
2012-10-07 ago detach tooltip as dockable window;
2012-10-07 ago explicit close button;
2012-10-05 ago further support for nested tooltips;
2012-10-05 ago refer to parent frame -- relevant for floating dockables in particular;
2012-10-05 ago tuned window position to fit on screen;
2012-10-05 ago tuned window position;
2012-10-05 ago determine window size from content;
2012-10-05 ago tuned color and font size;
2012-10-05 ago close tooltip window on escape;
2012-10-04 ago some re-ordering of initialization to ensure proper formatting;
2012-10-04 ago separate module Pretty_Tooltip;