equal
deleted
inserted
replaced
193 val path = Path.explode(text) |
193 val path = Path.explode(text) |
194 val (dir, base_name) = |
194 val (dir, base_name) = |
195 if (text == "" || text.endsWith("/")) (path, "") |
195 if (text == "" || text.endsWith("/")) (path, "") |
196 else (path.dir, path.base.implode) |
196 else (path.dir, path.base.implode) |
197 |
197 |
198 val directory = |
198 val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir)) |
199 new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir)) |
|
200 val files = directory.listFiles |
199 val files = directory.listFiles |
201 if (files == null) Nil |
200 if (files == null) Nil |
202 else { |
201 else { |
203 val ignore = |
202 val ignore = |
204 Library.space_explode(':', PIDE.options.string("jedit_completion_path_ignore")). |
203 Library.space_explode(':', PIDE.options.string("jedit_completion_path_ignore")). |