| Mon, 22 Aug 2022 14:48:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 14:29:59 +0200 |
wenzelm |
more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2022 15:56:14 +0200 |
wenzelm |
tuned -- avoid warnings for scala3;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2021 15:34:54 +0100 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
file |
diff |
annotate
|
| Sun, 14 Nov 2021 15:21:40 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Wed, 16 Dec 2020 13:22:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2020 22:01:54 +0100 |
wenzelm |
clarified caret focus modifier, depending on option "jedit_focus_modifier";
|
file |
diff |
annotate
|
| Mon, 14 Dec 2020 16:51:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2020 16:40:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2020 23:11:41 +0100 |
wenzelm |
unused (see 29566b6810f7);
|
file |
diff |
annotate
|
| Sun, 13 Dec 2020 23:06:33 +0100 |
wenzelm |
proper argument --- amending 908d8be90533;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2020 22:54:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2020 22:43:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|