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
|