Tue, 02 Dec 2014 16:40:11 +0100 | wenzelm | tuned signature -- more explicit types; | file | diff | annotate |
Sun, 11 May 2014 20:23:08 +0200 | wenzelm | more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion; | file | diff | annotate |
Thu, 08 May 2014 00:14:06 +0200 | wenzelm | some odd tricks to provide "Detach" menu item, via "PIDE" docking framework; | file | diff | annotate |