| Thu, 07 Nov 2024 12:08:32 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2024 12:22:24 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2024 11:21:04 +0100 |
wenzelm |
tuned GUI (again, see 0521e65af41e);
|
file |
diff |
annotate
|
| Sun, 03 Nov 2024 19:38:30 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2024 14:11:01 +0100 |
wenzelm |
tuned GUI;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2024 20:24:53 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2024 20:14:44 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2024 15:59:48 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2024 13:33:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 27 Dec 2022 12:00:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2022 12:25:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2022 12:21:44 +0100 |
wenzelm |
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2022 11:20:37 +0100 |
wenzelm |
clarified signature: only support nameless separator;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2022 11:17:26 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 21:14:20 +0100 |
wenzelm |
more robust selection: avoid duplicates via "batch" number;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 19:42:21 +0100 |
wenzelm |
clarified GUI.Selector, with support for separator as pseudo-entry;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 23:08:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 23:04:53 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 22:41:45 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 12:32:38 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 11:35:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2021 22:14:27 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Fri, 25 Jun 2021 21:33:21 +0200 |
wenzelm |
avoid deprecated operation;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
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
|
| Sat, 09 Jan 2021 20:17:56 +0100 |
wenzelm |
clarified list of presented look-and-feels;
|
file |
diff |
annotate
|
| Sat, 09 Jan 2021 19:49:22 +0100 |
wenzelm |
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 23:59:28 +0100 |
wenzelm |
support for additional look-and-feels;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2021 13:28:13 +0100 |
wenzelm |
clarified dock icon: setup earlier on startup;
|
file |
diff |
annotate
|
| Tue, 05 Jan 2021 22:05:18 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Tue, 05 Jan 2021 21:58:00 +0100 |
wenzelm |
prefer official Java 9 operations;
|
file |
diff |
annotate
|
| Tue, 05 Jan 2021 21:46:35 +0100 |
wenzelm |
proper dock icon for macOS;
|
file |
diff |
annotate
|
| Sun, 03 Jan 2021 23:01:16 +0100 |
wenzelm |
some attempts at multi-platform full-screen mode;
|
file |
diff |
annotate
|
| Sun, 03 Jan 2021 22:06:19 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 21 Dec 2020 22:03:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 21 Dec 2020 21:56:20 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 29 Nov 2020 23:23:32 +0100 |
wenzelm |
more Isabelle fonts, notably for PanelWindowContainer buttons with Windows L&F;
|
file |
diff |
annotate
|
| Thu, 09 Jan 2020 16:01:31 +0100 |
wenzelm |
proper name;
|
file |
diff |
annotate
|
| Thu, 09 Jan 2020 15:45:31 +0100 |
wenzelm |
more Isabelle fonts, notably for File Browser title in GTK L&F;
|
file |
diff |
annotate
|
| Thu, 09 Jan 2020 13:39:33 +0100 |
wenzelm |
tuned -- more direct java.util.Map.of;
|
file |
diff |
annotate
|
| Sat, 01 Dec 2018 16:57:46 +0100 |
wenzelm |
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2018 15:02:31 +0100 |
wenzelm |
more Isabelle fonts;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2018 14:46:00 +0100 |
wenzelm |
use Isabelle fonts for all GUI look-and-feels;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2018 14:21:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2018 16:27:21 +0100 |
wenzelm |
clarified signature: fonts are not dependent on GUI;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2018 14:00:22 +0100 |
wenzelm |
more explicit Isabelle_Fonts.Entry;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2018 12:05:50 +0100 |
wenzelm |
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2018 11:43:06 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2018 11:28:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2018 18:56:44 +0100 |
wenzelm |
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2018 12:28:09 +0200 |
wenzelm |
unused -- avoid illegal access in Java 11;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2018 11:17:59 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 18:43:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 02 Mar 2017 15:56:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2016 20:47:17 +0200 |
wenzelm |
handle font-size events;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2016 12:02:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 09 Jan 2016 22:00:22 +0100 |
wenzelm |
tuned -- according to ML version;
|
file |
diff |
annotate
|
| Mon, 23 Nov 2015 19:51:33 +0100 |
wenzelm |
clarified font: GUI defaults might change dynamically;
|
file |
diff |
annotate
|