| Sat, 08 Apr 2023 20:26:32 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 11:51:04 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 20:26:28 +0100 |
wenzelm |
clarified generic path operations;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 16:23:32 +0100 |
wenzelm |
more flexible: implicit support for Windows;
|
file |
diff |
annotate
|
| Sun, 11 Dec 2022 14:16:09 +0100 |
wenzelm |
tuned: less redundant implementation;
|
file |
diff |
annotate
|
| Sun, 11 Dec 2022 13:46:34 +0100 |
wenzelm |
clarified signature: more general operations;
|
file |
diff |
annotate
|
| Sun, 11 Dec 2022 12:52:46 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 19:05:48 +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
|
| Fri, 12 Mar 2021 23:00:01 +0100 |
wenzelm |
clarified HTTP.Content: support encoding;
|
file |
diff |
annotate
|
| Fri, 12 Mar 2021 19:46:37 +0100 |
wenzelm |
clarified signature: more explicit HTTP operations;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Sat, 07 Nov 2020 20:24:34 +0100 |
wenzelm |
support for Mailman list servers;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Mon, 25 Nov 2019 12:19:14 +0100 |
wenzelm |
tuned -- avoid deprecated constructors;
|
file |
diff |
annotate
|
| Mon, 11 Mar 2019 22:13:14 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 03 Dec 2018 15:15:54 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Thu, 21 Dec 2017 21:44:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 30 Jun 2017 14:26:45 +0200 |
wenzelm |
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
|
file |
diff |
annotate
|
| Fri, 30 Jun 2017 14:19:37 +0200 |
wenzelm |
clarified platform file operations;
|
file |
diff |
annotate
|
| Sat, 11 Mar 2017 20:18:06 +0100 |
wenzelm |
more complete exception handling;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 17:48:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 19:42:08 +0100 |
wenzelm |
clarified Document.Node.Name (again): canonical platform file;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 12:03:45 +0100 |
wenzelm |
clarified file URIs;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2017 19:22:17 +0100 |
wenzelm |
clarified file URLs, notably for Windows UNC paths;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2017 14:17:03 +0100 |
wenzelm |
clarified master_dir: file-URL;
|
file |
diff |
annotate
|
| Sun, 01 Jan 2017 11:47:27 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 01 Jan 2017 11:38:29 +0100 |
wenzelm |
clarified file URI operations;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2016 23:19:35 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2016 20:35:21 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Wed, 27 Jan 2016 14:14:06 +0100 |
wenzelm |
allow single quote within URL;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 10:06:54 +0200 |
wenzelm |
no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 23:04:20 +0200 |
wenzelm |
basic URL operations (with Isabelle/Scala error handling);
|
file |
diff |
annotate
|