equal
deleted
inserted
replaced
44 |
44 |
45 |
45 |
46 /* external file */ |
46 /* external file */ |
47 |
47 |
48 val file: JFile = VSCode_Resources.canonical_file(uri) |
48 val file: JFile = VSCode_Resources.canonical_file(uri) |
|
49 |
|
50 def external(b: Boolean): Document_Model = copy(external_file = b) |
49 |
51 |
50 def register(watcher: File_Watcher) |
52 def register(watcher: File_Watcher) |
51 { |
53 { |
52 val dir = file.getParentFile |
54 val dir = file.getParentFile |
53 if (dir != null && dir.isDirectory) watcher.register(dir) |
55 if (dir != null && dir.isDirectory) watcher.register(dir) |