2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-05-09 wenzelm 2014-05-09 tuned signature;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-09 wenzelm 2014-04-09 dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
2014-03-31 wenzelm 2014-03-31 observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;
2014-03-01 wenzelm 2014-03-01 tuned signature -- separate module Font_Info;
2013-11-08 wenzelm 2013-11-08 transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
2013-09-21 wenzelm 2013-09-21 tuned;
2013-09-21 wenzelm 2013-09-21 proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
2013-09-18 wenzelm 2013-09-18 tuned signature;
2013-08-28 wenzelm 2013-08-28 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-27 wenzelm 2013-08-27 determine completion geometry like tooltip; just one option jedit_popup_bounds for tooltip and completion;
2013-08-27 wenzelm 2013-08-27 explicit "hidden" operation with focus management; explicit popup_font; just one option jedit_popup_font_scale for tooltip and completion;
2013-08-25 wenzelm 2013-08-25 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 wenzelm 2013-08-24 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 wenzelm 2013-08-13 more general window_geometry;
2013-08-13 wenzelm 2013-08-13 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/;
2013-08-05 wenzelm 2013-08-05 tuned signature;
2013-07-15 wenzelm 2013-07-15 deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
2013-07-07 wenzelm 2013-07-07 some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
2013-07-01 wenzelm 2013-07-01 clarified focus after dismiss;
2013-07-01 wenzelm 2013-07-01 tuned signature;
2013-07-01 wenzelm 2013-07-01 avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
2013-07-01 wenzelm 2013-07-01 clarified tooltip timing of pending event and active state;
2013-07-01 wenzelm 2013-07-01 less intrusive border, notably on windows;
2013-07-01 wenzelm 2013-07-01 tighten tooltip size;
2013-07-01 wenzelm 2013-07-01 visually explicit focus (behaviour dependent on platform and look-and-feel);
2013-06-29 wenzelm 2013-06-29 avoid potential race condition of focusLost/dismiss vs.;
2013-06-29 wenzelm 2013-06-29 more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
2013-06-29 wenzelm 2013-06-29 update text only once;
2013-06-29 wenzelm 2013-06-29 tuned signature;
2013-06-29 wenzelm 2013-06-29 manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6); more explicit tooltip hierarchy: manage exactly the visible stack -- caching is part of PopupFactory; auxiliary geometry measurement via single hidden window; tuned signature;
2013-06-28 wenzelm 2013-06-28 load icons via options -- prefer IntelliJ IDEA for now;
2013-03-23 wenzelm 2013-03-23 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23 wenzelm 2013-03-23 allow fractional pretty margin -- avoid premature rounding;
2013-03-23 wenzelm 2013-03-23 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); separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
2013-03-18 wenzelm 2013-03-18 prefer ownerless window, to avoid question of potentially changing parent view;
2013-03-18 wenzelm 2013-03-18 proper parent component for window.init;
2013-03-18 wenzelm 2013-03-18 extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
2013-03-18 wenzelm 2013-03-18 recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
2013-03-17 wenzelm 2013-03-17 re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;
2013-03-17 wenzelm 2013-03-17 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 wenzelm 2013-03-16 some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;
2013-03-16 wenzelm 2013-03-16 more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible); more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors); early initialization of gutter to get proper text area painter size (see also 2585c81d840a);
2013-01-16 wenzelm 2013-01-16 close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
2013-01-12 wenzelm 2013-01-12 more uniform Pretty.char_width;
2013-01-05 wenzelm 2013-01-05 propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
2013-01-04 wenzelm 2013-01-04 more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
2012-12-31 wenzelm 2012-12-31 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 wenzelm 2012-12-15 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment; more tooltip options via Rendering;
2012-12-14 wenzelm 2012-12-14 init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-11-25 wenzelm 2012-11-25 tuned signature; uniform view.fontsize fallback;
2012-11-25 wenzelm 2012-11-25 renamed main plugin object to PIDE;
2012-11-25 wenzelm 2012-11-25 quasi-abstract module Rendering, with Isabelle-specific implementation;
2012-11-22 wenzelm 2012-11-22 pack window before accessing its geometry;
2012-11-22 wenzelm 2012-11-22 more precise tooltip window size;
2012-11-21 wenzelm 2012-11-21 tuned;
2012-10-13 wenzelm 2012-10-13 improved adhoc height for small fonts;
2012-10-12 wenzelm 2012-10-12 more uniform tooltip color;