| Fri, 05 Jul 2024 11:38:21 +0200 |
wenzelm |
prefer official UTF-8 decoding (in contrast to 2541de190d92): this is also more efficient (factor 10-20);
|
file |
diff |
annotate
|
| Wed, 03 Jul 2024 21:11:53 +0200 |
wenzelm |
clarified signature, following 43323d886ea3;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2024 20:35:10 +0200 |
wenzelm |
clarified signature: more direct Bytes.raw and subsequent UTF-8 default decoding;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2024 15:24:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Jun 2024 13:46:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Jun 2024 13:14:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Jun 2024 23:24:24 +0200 |
wenzelm |
notable performance tuning: avoid overhead of higher-order functions;
|
file |
diff |
annotate
|
| Sat, 15 Jun 2024 20:44:09 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sat, 15 Jun 2024 20:29:50 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 11 Jun 2024 16:39:53 +0200 |
wenzelm |
clarified signature (again);
|
file |
diff |
annotate
|
| Tue, 11 Jun 2024 16:02:33 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Tue, 11 Jun 2024 15:49:39 +0200 |
wenzelm |
clarified signature: more accurate types;
|
file |
diff |
annotate
|
| Tue, 11 Jun 2024 14:18:19 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 19:14:01 +0200 |
wenzelm |
tuned signature, following isabelle.setup.Environment;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 19:10:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 19:08:18 +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
|
| Mon, 12 Apr 2021 12:16:49 +0200 |
wenzelm |
clarified signature: Bytes extends CharSequence already (see d201996f72a8);
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2021 13:04:29 +0100 |
wenzelm |
more informative errors: simplify diagnosis of spurious failures reported by users;
|
file |
diff |
annotate
|
| Sun, 20 May 2018 11:57:17 +0200 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
| Sun, 12 Mar 2017 14:23:38 +0100 |
wenzelm |
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 11:21:46 +0100 |
wenzelm |
clarified directories;
|
file |
diff |
annotate
| base
|