src/Tools/jEdit/src/pretty_tooltip.scala
2014-07-23 ago clarified module name: facilitate alternative GUI frameworks;
2014-05-09 ago tuned signature;
2014-04-22 ago avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-09 ago dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
2014-03-31 ago observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
2014-03-01 ago tuned signature -- separate module Font_Info;
2013-11-08 ago transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
2013-09-21 ago tuned;
2013-09-21 ago proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
2013-09-18 ago tuned signature;
2013-08-28 ago uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-27 ago determine completion geometry like tooltip;
2013-08-27 ago explicit "hidden" operation with focus management;
2013-08-25 ago use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);
2013-08-24 ago confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;
2013-08-13 ago more general window_geometry;
2013-08-13 ago 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);
2013-08-05 ago tuned signature;
2013-07-15 ago deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
2013-07-07 ago some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
2013-07-01 ago clarified focus after dismiss;
2013-07-01 ago tuned signature;
2013-07-01 ago avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
2013-07-01 ago clarified tooltip timing of pending event and active state;
2013-07-01 ago less intrusive border, notably on windows;
2013-07-01 ago tighten tooltip size;
2013-07-01 ago visually explicit focus (behaviour dependent on platform and look-and-feel);
2013-06-29 ago avoid potential race condition of focusLost/dismiss vs. popup.show;
2013-06-29 ago more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
2013-06-29 ago update text only once;
2013-06-29 ago tuned signature;
2013-06-29 ago manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
2013-06-28 ago load icons via options -- prefer IntelliJ IDEA for now;
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;