2013-03-25 wenzelm 2013-03-25 tuned signature;
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-21 wenzelm 2013-03-21 eliminated char_width_int to avoid unclear rounding; clarified integer conversion for margin;
2013-02-06 wenzelm 2013-02-06 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
2013-01-12 wenzelm 2013-01-12 more uniform Pretty.char_width;
2012-12-31 wenzelm 2012-12-31 tuned signature;
2012-12-16 wenzelm 2012-12-16 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
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-05 wenzelm 2012-12-05 tuned signature in accordance to document operations;
2012-11-26 wenzelm 2012-11-26 more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
2012-11-24 wenzelm 2012-11-24 prefer buffer_edit combinator over Java-style boilerplate;
2012-11-24 wenzelm 2012-11-24 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
2012-11-18 wenzelm 2012-11-18 more accurate pixel_range -- do not round offset here;
2012-11-18 wenzelm 2012-11-18 tuned signature;
2012-10-19 wenzelm 2012-10-19 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
2012-10-12 wenzelm 2012-10-12 further refinement of jEdit line range, avoiding lack of final \n;
2012-10-05 wenzelm 2012-10-05 further support for nested tooltips;
2012-10-05 wenzelm 2012-10-05 refer to parent frame -- relevant for floating dockables in particular;
2012-09-17 wenzelm 2012-09-17 tuned signature;
2012-09-17 wenzelm 2012-09-17 tuned signature;
2012-09-17 wenzelm 2012-09-17 tuned signature;
2012-09-17 wenzelm 2012-09-17 somewhat more general JEdit_Lib; tuned signatures;