src/Tools/jEdit/src/pretty_tooltip.scala
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