src/Tools/jEdit/src/jedit_resources.scala
changeset 76864 56c926de7ea6
parent 76860 f95ed5a0600c
child 76890 d924a69e7d2b
equal deleted inserted replaced
76863:13b2d8961f8a 76864:56c926de7ea6
    48   }
    48   }
    49 
    49 
    50   override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
    50   override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
    51     node_name(File.platform_path(Path.explode(standard_name.node).canonical))
    51     node_name(File.platform_path(Path.explode(standard_name.node).canonical))
    52 
    52 
    53   override def append_path(dir: String, source_path: Path): String = {
    53   override def append_path(prefix: String, source_path: Path): String = {
    54     val path = source_path.expand
    54     val path = source_path.expand
    55     if (dir == "" || path.is_absolute) {
    55     if (prefix == "" || path.is_absolute) {
    56       MiscUtilities.resolveSymlinks(File.platform_path(path))
    56       MiscUtilities.resolveSymlinks(File.platform_path(path))
    57     }
    57     }
    58     else if (path.is_current) dir
    58     else if (path.is_current) prefix
    59     else {
    59     else {
    60       val vfs = VFSManager.getVFSForPath(dir)
    60       val vfs = VFSManager.getVFSForPath(prefix)
    61       if (vfs.isInstanceOf[FileVFS]) {
    61       if (vfs.isInstanceOf[FileVFS]) {
    62         MiscUtilities.resolveSymlinks(
    62         MiscUtilities.resolveSymlinks(
    63           vfs.constructPath(dir, File.platform_path(path)))
    63           vfs.constructPath(prefix, File.platform_path(path)))
    64       }
    64       }
    65       else vfs.constructPath(dir, File.standard_path(path))
    65       else vfs.constructPath(prefix, File.standard_path(path))
    66     }
    66     }
    67   }
    67   }
    68 
    68 
    69 
    69 
    70   /* file content */
    70   /* file content */