src/Tools/jEdit/src/jedit_resources.scala
changeset 60988 1d7a7e33fd67
parent 60917 0607869c2ff3
child 61023 46df28442a80
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 20 17:41:50 2015 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 20 19:15:17 2015 +0200
     1.3 @@ -56,14 +56,14 @@
     1.4    {
     1.5      val path = source_path.expand
     1.6      if (dir == "" || path.is_absolute)
     1.7 -      MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path))
     1.8 +      MiscUtilities.resolveSymlinks(File.platform_path(path))
     1.9      else if (path.is_current) dir
    1.10      else {
    1.11        val vfs = VFSManager.getVFSForPath(dir)
    1.12        if (vfs.isInstanceOf[FileVFS])
    1.13          MiscUtilities.resolveSymlinks(
    1.14 -          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
    1.15 -      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
    1.16 +          vfs.constructPath(dir, File.platform_path(path)))
    1.17 +      else vfs.constructPath(dir, File.standard_path(path))
    1.18      }
    1.19    }
    1.20