| 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
|