src/Pure/GUI/gui.scala
Thu, 24 Jul 2014 11:46:40 +0200 wenzelm tuned;
Wed, 23 Jul 2014 11:19:24 +0200 wenzelm clarified module name: facilitate alternative GUI frameworks;
Wed, 21 May 2014 16:21:11 +0200 wenzelm more uniform Font_Info.Zoom_Box;
Tue, 06 May 2014 23:35:24 +0200 wenzelm tuned GUI for Windows L&F;
Tue, 06 May 2014 15:54:22 +0200 wenzelm tuned GUI layout;
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;
Sat, 19 Apr 2014 19:03:32 +0200 wenzelm clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
less more (0) -10 -7 tip