| Thu, 09 Jan 2020 13:39:33 +0100 |
wenzelm |
tuned -- more direct java.util.Map.of;
|
file |
diff |
annotate
|
| Thu, 11 Apr 2019 17:07:52 +0200 |
wenzelm |
visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937);
|
file |
diff |
annotate
|
| Sun, 24 Mar 2019 18:30:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2017 22:52:16 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2017 18:30:28 +0100 |
wenzelm |
clarified control style;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2017 17:37:26 +0100 |
wenzelm |
font style for literal control symbols, notably for antiquotations;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2017 16:28:00 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Mon, 06 Nov 2017 16:03:13 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 13:19:14 +0200 |
wenzelm |
uniform notion of Symbol.is_controllable (see also 265d9300d523);
|
file |
diff |
annotate
|
| Thu, 01 Jun 2017 21:15:56 +0200 |
wenzelm |
output control symbols like ML version, with optionally hidden source;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2017 16:55:37 +0100 |
wenzelm |
keep style extender for the sake of potentially remaining token markers;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2017 14:08:36 +0100 |
wenzelm |
clarified initialization;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2017 13:49:39 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2017 13:35:14 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|