| 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 |