| Sat, 18 May 2013 12:41:31 +0200 | wenzelm | explicit notion of public options, which are shown in the editor options dialog; | file | diff | annotate |
| Thu, 04 Apr 2013 17:58:47 +0200 | wenzelm | tuned signature -- concentrate GUI tools; | file | diff | annotate |
| Thu, 04 Oct 2012 19:31:50 +0200 | wenzelm | refined rich tooltip options; | file | diff | annotate |
| Fri, 14 Sep 2012 13:52:16 +0200 | wenzelm | more static handling of rendering options; | file | diff | annotate |
| Wed, 12 Sep 2012 11:14:44 +0200 | wenzelm | tuned error; | file | diff | annotate |
| Tue, 11 Sep 2012 23:26:03 +0200 | wenzelm | some GUI support for color options; | file | diff | annotate |
| Tue, 11 Sep 2012 19:35:21 +0200 | wenzelm | more informative tooltip: default value; | file | diff | annotate |