src/Tools/jEdit/src/info_dockable.scala
2014-04-25 wenzelm 2014-04-25 clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; eliminated old actors;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-03-01 wenzelm 2014-03-01 tuned signature -- separate module Font_Info;
2014-02-20 wenzelm 2014-02-20 tuned imports;
2013-09-18 wenzelm 2013-09-18 tuned signature;
2013-09-18 wenzelm 2013-09-18 improved FlowLayout for wrapping of components over multiple lines;
2013-08-24 wenzelm 2013-08-24 more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
2013-08-12 wenzelm 2013-08-12 tuned signature;
2013-08-08 wenzelm 2013-08-08 tuned imports;
2013-04-04 wenzelm 2013-04-04 tuned signature -- concentrate GUI tools;
2012-12-14 wenzelm 2012-12-14 more formal class Command.Results;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-12-10 wenzelm 2012-12-10 tuned;
2012-11-25 wenzelm 2012-11-25 tuned signature;
2012-11-25 wenzelm 2012-11-25 tuned signature; uniform view.fontsize fallback;
2012-11-25 wenzelm 2012-11-25 renamed main plugin object to PIDE;
2012-11-21 wenzelm 2012-11-21 tuned;
2012-11-18 wenzelm 2012-11-18 update options via protocol; jEdit dialog for "Parallel Checking" options;
2012-10-16 wenzelm 2012-10-16 retain info dockable state via educated guess on window focus;
2012-10-07 wenzelm 2012-10-07 detach tooltip as dockable window;