always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
authorwenzelm
Sat Aug 02 12:24:30 2014 +0200 (2014-08-02 ago)
changeset 57841e212e2001b2a
parent 57840 074cb68b40a8
child 57842 8e4ae2db1849
always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Aug 02 11:39:13 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Aug 02 12:24:30 2014 +0200
     1.3 @@ -49,7 +49,8 @@
     1.4    override def append(dir: String, source_path: Path): String =
     1.5    {
     1.6      val path = source_path.expand
     1.7 -    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
     1.8 +    if (dir == "" || path.is_absolute)
     1.9 +      MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path))
    1.10      else if (path.is_current) dir
    1.11      else {
    1.12        val vfs = VFSManager.getVFSForPath(dir)