| Mon, 05 Jan 2015 14:13:38 +0100 |
wenzelm |
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2015 17:27:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 11:50:34 +0100 |
wenzelm |
added system property isabelle.laf, notably for initial system dialog;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2014 16:00:38 +0100 |
wenzelm |
imitate font more carefully: err on smaller size;
|
file |
diff |
annotate
|
| Tue, 02 Dec 2014 17:30:53 +0100 |
wenzelm |
added Untyped.method convenience (for *this* class only);
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 12:06:22 +0200 |
wenzelm |
separate Java FX modules -- no need to include jfxrt.jar by default;
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 13:59:08 +0200 |
wenzelm |
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
|
file |
diff |
annotate
|
| 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
|
| Fri, 10 Jan 2014 12:29:25 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|