omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;
--- a/src/Tools/jEdit/src/plugin.scala Mon Aug 15 19:42:52 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 16 12:06:49 2011 +0200
@@ -334,8 +334,8 @@
else {
val vfs = VFSManager.getVFSForPath(master_dir)
if (vfs.isInstanceOf[FileVFS])
- MiscUtilities.resolveSymlinks(
- vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
+ vfs.constructPath(master_dir, Isabelle_System.platform_path(path))
+ // FIXME MiscUtilities.resolveSymlinks (!?)
else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
}
}