src/Tools/jEdit/src/pide_docking_framework.scala
Tue, 02 Dec 2014 16:40:11 +0100 wenzelm tuned signature -- more explicit types;
Sun, 11 May 2014 20:23:08 +0200 wenzelm more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
Thu, 08 May 2014 00:14:06 +0200 wenzelm some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
less more (0) tip