| Tue, 06 May 2014 21:29:17 +0200 |
wenzelm |
common support for search field, which is actually a light-weight Highlighter;
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 12:51:08 +0200 |
wenzelm |
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
|
file |
diff |
annotate
|
| Tue, 22 Apr 2014 23:49:15 +0200 |
wenzelm |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 19:39:27 +0100 |
wenzelm |
tuned signature -- separate module Font_Info;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 14:36:17 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 15:50:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 15:09:15 +0200 |
wenzelm |
improved FlowLayout for wrapping of components over multiple lines;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 13:32:51 +0200 |
wenzelm |
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 11:49:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 14:13:04 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2013 17:58:47 +0200 |
wenzelm |
tuned signature -- concentrate GUI tools;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:09:08 +0100 |
wenzelm |
more formal class Command.Results;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 15:13:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 21:23:20 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 21:10:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2012 14:06:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 15:28:58 +0100 |
wenzelm |
update options via protocol;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 22:13:46 +0200 |
wenzelm |
retain info dockable state via educated guess on window focus;
|
file |
diff |
annotate
|
| Sun, 07 Oct 2012 16:05:31 +0200 |
wenzelm |
detach tooltip as dockable window;
|
file |
diff |
annotate
|