| Sat, 11 Mar 2023 11:24:02 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 30 Jan 2023 16:26:10 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2022 16:26:59 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2022 16:23:49 +0100 |
wenzelm |
more uniform session selectors, with persistent options;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2022 16:25:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2022 16:14:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2022 15:59:06 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 23:47:08 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 23:08:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 22:41:45 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 21:43:45 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 21:23:59 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 18:06:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 17:18:45 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 14:45:36 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 19:47:38 +0200 |
wenzelm |
tuned, following hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 19:41:52 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2017 19:46:53 +0100 |
wenzelm |
afford early initialization of JEdit_Options, but it may lead to messy exception trace for malformed etc/preferences (see also 6eeaaefcea56);
|
file |
diff |
annotate
|
| 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
|