| Thu, 13 Feb 2025 16:19:48 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2025 14:16:11 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Fri, 24 May 2024 19:15:51 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 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
|