src/Tools/jEdit/src/info_dockable.scala
Tue, 27 Jun 2017 21:56:56 +0200 wenzelm clarified defaults;
Tue, 27 Jun 2017 21:36:58 +0200 wenzelm tuned signature;
Tue, 10 Jan 2017 16:03:50 +0100 wenzelm tuned;
Fri, 17 Jul 2015 21:45:15 +0200 wenzelm more uniform ComponentAdapter;
Wed, 23 Jul 2014 11:19:24 +0200 wenzelm clarified module name: facilitate alternative GUI frameworks;
Wed, 21 May 2014 16:21:11 +0200 wenzelm more uniform Font_Info.Zoom_Box;
Wed, 21 May 2014 14:42:45 +0200 wenzelm tuned signature;
Tue, 06 May 2014 21:29:17 +0200 wenzelm common support for search field, which is actually a light-weight Highlighter;
Fri, 25 Apr 2014 12:51:08 +0200 wenzelm clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
Tue, 22 Apr 2014 23:49:15 +0200 wenzelm avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
Sat, 01 Mar 2014 19:39:27 +0100 wenzelm tuned signature -- separate module Font_Info;
Thu, 20 Feb 2014 14:36:17 +0100 wenzelm tuned imports;
Wed, 18 Sep 2013 15:50:59 +0200 wenzelm tuned signature;
Wed, 18 Sep 2013 15:09:15 +0200 wenzelm improved FlowLayout for wrapping of components over multiple lines;
Sat, 24 Aug 2013 13:32:51 +0200 wenzelm more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
Mon, 12 Aug 2013 11:49:58 +0200 wenzelm tuned signature;
Thu, 08 Aug 2013 14:13:04 +0200 wenzelm tuned imports;
Thu, 04 Apr 2013 17:58:47 +0200 wenzelm tuned signature -- concentrate GUI tools;
Fri, 14 Dec 2012 12:09:08 +0100 wenzelm more formal class Command.Results;
Thu, 13 Dec 2012 17:29:23 +0100 wenzelm more careful handling of Dialog_Result, with active area and color feedback;
Mon, 10 Dec 2012 15:13:13 +0100 wenzelm tuned;
Sun, 25 Nov 2012 21:23:20 +0100 wenzelm tuned signature;
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