src/Tools/jEdit/src/pretty_tooltip.scala
Sat, 13 Oct 2012 00:08:36 +0200 wenzelm improved adhoc height for small fonts;
Fri, 12 Oct 2012 22:53:20 +0200 wenzelm more uniform tooltip color;
Mon, 08 Oct 2012 12:40:35 +0200 wenzelm use Pretty_Tooltip for Graphview_Panel;
Sun, 07 Oct 2012 16:26:31 +0200 wenzelm close tooltips more thoroughly;
Sun, 07 Oct 2012 16:15:31 +0200 wenzelm make buttons closer to original mouse position;
Sun, 07 Oct 2012 16:05:31 +0200 wenzelm detach tooltip as dockable window;
Sun, 07 Oct 2012 15:05:11 +0200 wenzelm explicit close button;
Fri, 05 Oct 2012 14:32:56 +0200 wenzelm further support for nested tooltips;
Fri, 05 Oct 2012 13:48:22 +0200 wenzelm refer to parent frame -- relevant for floating dockables in particular;
Fri, 05 Oct 2012 12:11:23 +0200 wenzelm tuned window position to fit on screen;
Fri, 05 Oct 2012 12:00:28 +0200 wenzelm tuned window position;
Fri, 05 Oct 2012 11:36:46 +0200 wenzelm determine window size from content;
Fri, 05 Oct 2012 11:09:24 +0200 wenzelm tuned color and font size;
Fri, 05 Oct 2012 10:54:07 +0200 wenzelm close tooltip window on escape;
Thu, 04 Oct 2012 20:36:10 +0200 wenzelm some re-ordering of initialization to ensure proper formatting;
Thu, 04 Oct 2012 20:14:40 +0200 wenzelm separate module Pretty_Tooltip;
less more (0) tip