| Thu, 21 Jan 2016 20:50:34 +0100 |
wenzelm |
clarified errors: more explicit treatment of uninitialized state;
|
file |
diff |
annotate
|
| Mon, 23 Nov 2015 19:51:33 +0100 |
wenzelm |
clarified font: GUI defaults might change dynamically;
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 22:16:04 +0100 |
wenzelm |
prefer static Font -- evade spontaneous change of TextField.font seen with Metal L&F in Plugin Options / Isabelle / General / Apply;
|
file |
diff |
annotate
|
| Wed, 05 Aug 2015 16:22:40 +0200 |
wenzelm |
proper initialization;
|
file |
diff |
annotate
|
| Wed, 05 Aug 2015 16:13:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
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
|
| Tue, 22 Apr 2014 23:49:15 +0200 |
wenzelm |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
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
|
| Thu, 17 Apr 2014 11:13:30 +0200 |
wenzelm |
proper tooltip_lines for multi-line text;
|
file |
diff |
annotate
|
| 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
|
| Tue, 11 Sep 2012 15:47:42 +0200 |
wenzelm |
some support to organize options in sections;
|
file |
diff |
annotate
|
| Tue, 11 Sep 2012 11:29:28 +0200 |
wenzelm |
prefer global default font over IsabelleText of jEdit TextArea;
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 19:56:08 +0200 |
wenzelm |
proper multi-line tooltip;
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 19:49:30 +0200 |
wenzelm |
more detailed option tooltip;
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 17:13:17 +0200 |
wenzelm |
more systematic JEdit_Options.make_component;
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 15:20:50 +0200 |
wenzelm |
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
|
file |
diff |
annotate
|