Fri, 30 Dec 2016 20:36:13 +0100 | wenzelm | manage changes of external files; | file | diff | annotate |
Fri, 30 Dec 2016 17:45:00 +0100 | wenzelm | more explicit edits -- eliminated Clear; | file | diff | annotate |
Fri, 30 Dec 2016 11:54:11 +0100 | wenzelm | tuned; | file | diff | annotate |
Fri, 30 Dec 2016 11:46:34 +0100 | wenzelm | clarified Document_Model perspective and edits; | file | diff | annotate |
Fri, 30 Dec 2016 10:26:10 +0100 | wenzelm | tuned; | file | diff | annotate |
Thu, 29 Dec 2016 22:10:29 +0100 | wenzelm | re-use options from resources; | file | diff | annotate |
Thu, 29 Dec 2016 21:54:04 +0100 | wenzelm | moved main state to VSCode_Resources; | file | diff | annotate |
Wed, 21 Dec 2016 11:41:05 +0100 | wenzelm | clarified node_name: preserve original uri; | file | diff | annotate |
Tue, 20 Dec 2016 22:32:04 +0100 | wenzelm | clarified module name; | file | diff | annotate | base |