| #
efea19a1 |
|
21-Dec-2017 |
wenzelm <none@none> |
tuned signature;
|
| #
8be91295 |
|
30-Jun-2017 |
wenzelm <none@none> |
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
|
| #
8e161900 |
|
30-Jun-2017 |
wenzelm <none@none> |
clarified platform file operations;
|
| #
0e9f9aec |
|
11-Mar-2017 |
wenzelm <none@none> |
more complete exception handling;
|
| #
e4ede68b |
|
28-Feb-2017 |
wenzelm <none@none> |
tuned;
|
| #
7e9a90d1 |
|
04-Jan-2017 |
wenzelm <none@none> |
clarified Document.Node.Name (again): canonical platform file;
identify document models by native java.io.File;
|
| #
d277e44b |
|
03-Jan-2017 |
wenzelm <none@none> |
clarified file URIs;
|
| #
15c32a03 |
|
03-Jan-2017 |
wenzelm <none@none> |
clarified file URLs, notably for Windows UNC paths;
|
| #
73946bbf |
|
03-Jan-2017 |
wenzelm <none@none> |
clarified master_dir: file-URL;
|
| #
b0986b49 |
|
01-Jan-2017 |
wenzelm <none@none> |
clarified modules;
|
| #
9833c7d2 |
|
01-Jan-2017 |
wenzelm <none@none> |
clarified file URI operations;
|
| #
eaecfa7d |
|
09-Aug-2016 |
wenzelm <none@none> |
more operations;
|
| #
dc020bce |
|
09-Aug-2016 |
wenzelm <none@none> |
more operations;
|
| #
8a39146a |
|
27-Jan-2016 |
wenzelm <none@none> |
allow single quote within URL;
|
| #
c880492b |
|
10-Apr-2014 |
wenzelm <none@none> |
no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;
|
| #
af57a3e5 |
|
09-Apr-2014 |
wenzelm <none@none> |
basic URL operations (with Isabelle/Scala error handling);
|