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