Thu, 24 Jul 2014 11:46:40 +0200 | wenzelm | tuned; | file | diff | annotate |
Wed, 23 Jul 2014 11:19:24 +0200 | wenzelm | clarified module name: facilitate alternative GUI frameworks; | file | diff | annotate |
Wed, 21 May 2014 16:21:11 +0200 | wenzelm | more uniform Font_Info.Zoom_Box; | file | diff | annotate |
Tue, 06 May 2014 23:35:24 +0200 | wenzelm | tuned GUI for Windows L&F; | file | diff | annotate |
Tue, 06 May 2014 15:54:22 +0200 | wenzelm | tuned GUI layout; | file | diff | annotate |
Sat, 26 Apr 2014 15:33:13 +0200 | wenzelm | uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice; | file | diff | annotate |
Sat, 19 Apr 2014 19:03:32 +0200 | wenzelm | clarified tooltip_lines: HTML.encode already takes care of newline (but not space); | file | diff | annotate |