src/Tools/VSCode/src/vscode_resources.scala
2017-01-09 wenzelm 2017-01-09 tuned signature;
2017-01-08 wenzelm 2017-01-08 tuned signature;
2017-01-08 wenzelm 2017-01-08 tuned;
2017-01-08 wenzelm 2017-01-08 support for bibtex entries;
2017-01-08 wenzelm 2017-01-08 more explocit Document_Model.Content;
2017-01-07 wenzelm 2017-01-07 tuned signature;
2017-01-07 wenzelm 2017-01-07 clarified lazy text content;
2017-01-07 wenzelm 2017-01-07 tuned;
2017-01-06 wenzelm 2017-01-06 tuned signature;
2017-01-05 wenzelm 2017-01-05 more robust treatment of logical lines;
2017-01-05 wenzelm 2017-01-05 manage document blobs as well;
2017-01-05 wenzelm 2017-01-05 tuned;
2017-01-04 wenzelm 2017-01-04 proper registration of implicitly loaded files;
2017-01-04 wenzelm 2017-01-04 tuned;
2017-01-04 wenzelm 2017-01-04 clarified Document.Node.Name (again): canonical platform file; identify document models by native java.io.File;
2017-01-04 wenzelm 2017-01-04 clarified file URIs;
2017-01-03 wenzelm 2017-01-03 clarified file URLs, notably for Windows UNC paths;
2017-01-03 wenzelm 2017-01-03 clarified master_dir: file-URL;
2017-01-02 wenzelm 2017-01-02 proper bootstrap name, e.g. for Pure.thy;
2017-01-01 wenzelm 2017-01-01 just one synchronized access to global state: works recursively on JVM; tuned;
2017-01-01 wenzelm 2017-01-01 clarified file URI operations;
2016-12-31 wenzelm 2016-12-31 automatically resolve dependencies from document models and file-system;
2016-12-31 wenzelm 2016-12-31 clarified;
2016-12-31 wenzelm 2016-12-31 tuned signature;
2016-12-31 wenzelm 2016-12-31 proper state update;
2016-12-31 wenzelm 2016-12-31 tuned;
2016-12-31 wenzelm 2016-12-31 tuned signature;
2016-12-31 wenzelm 2016-12-31 proper import_name;
2016-12-30 wenzelm 2016-12-30 manage changes of external files; tuned;
2016-12-30 wenzelm 2016-12-30 more explicit edits -- eliminated Clear;
2016-12-30 wenzelm 2016-12-30 tuned;
2016-12-30 wenzelm 2016-12-30 clarified Document_Model perspective and edits;
2016-12-30 wenzelm 2016-12-30 tuned;
2016-12-29 wenzelm 2016-12-29 re-use options from resources;
2016-12-29 wenzelm 2016-12-29 moved main state to VSCode_Resources; misc tuning;
2016-12-21 wenzelm 2016-12-21 clarified node_name: preserve original uri;
2016-12-20 wenzelm 2016-12-20 clarified module name;