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, 02 Aug 2014 12:24:30 +0200
changeset 57841 e212e2001b2a
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
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Aug 02 11:39:13 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Aug 02 12:24:30 2014 +0200
@@ -49,7 +49,8 @@
   override def append(dir: String, source_path: Path): String =
   {
     val path = source_path.expand
-    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
+    if (dir == "" || path.is_absolute)
+      MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path))
     else if (path.is_current) dir
     else {
       val vfs = VFSManager.getVFSForPath(dir)