equal
deleted
inserted
replaced
47 /* file-system operations */ |
47 /* file-system operations */ |
48 |
48 |
49 override def append(dir: String, source_path: Path): String = |
49 override def append(dir: String, source_path: Path): String = |
50 { |
50 { |
51 val path = source_path.expand |
51 val path = source_path.expand |
52 if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path) |
52 if (dir == "" || path.is_absolute) |
|
53 MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path)) |
53 else if (path.is_current) dir |
54 else if (path.is_current) dir |
54 else { |
55 else { |
55 val vfs = VFSManager.getVFSForPath(dir) |
56 val vfs = VFSManager.getVFSForPath(dir) |
56 if (vfs.isInstanceOf[FileVFS]) |
57 if (vfs.isInstanceOf[FileVFS]) |
57 MiscUtilities.resolveSymlinks( |
58 MiscUtilities.resolveSymlinks( |