src/Tools/jEdit/src/completion_popup.scala
changeset 65488 331f09d9535e
parent 65239 509a9b0ad02e
child 65999 ee4cf96a9406
equal deleted inserted replaced
65487:7847807b07ce 65488:331f09d9535e
   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")).