src/Tools/jEdit/src/info_dockable.scala
Sun, 25 Nov 2012 21:10:29 +0100 wenzelm tuned signature;
Sun, 25 Nov 2012 20:59:32 +0100 wenzelm renamed main plugin object to PIDE;
Wed, 21 Nov 2012 14:06:59 +0100 wenzelm tuned;
Sun, 18 Nov 2012 15:28:58 +0100 wenzelm update options via protocol;
Tue, 16 Oct 2012 22:13:46 +0200 wenzelm retain info dockable state via educated guess on window focus;
Sun, 07 Oct 2012 16:05:31 +0200 wenzelm detach tooltip as dockable window;
less more (0) tip