| Mon, 22 Jan 2024 22:18:20 +0100 |
wenzelm |
recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL);
|
file |
diff |
annotate
|
| Sun, 21 Jan 2024 14:12:14 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 21 Jan 2024 14:05:14 +0100 |
wenzelm |
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
|
file |
diff |
annotate
|
| Fri, 24 Nov 2023 11:10:31 +0100 |
wenzelm |
more robust exception handling (amending 8cc1ae43e12e);
|
file |
diff |
annotate
|
| Thu, 23 Nov 2023 11:40:49 +0100 |
wenzelm |
clarified signature: avoid deprecated URL constructors;
|
file |
diff |
annotate
|
| 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
|