# HG changeset patch # User wenzelm # Date 1670492643 -3600 # Node ID ec505888434740d4d48d5830f89867c144c32ef0 # Parent 5af17ce5d297741253c781ae2836ae571ba94a3c tuned; diff -r 5af17ce5d297 -r ec5058884347 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Wed Dec 07 21:35:06 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Dec 08 10:44:03 2022 +0100 @@ -55,14 +55,16 @@ override def append(dir: String, source_path: Path): String = { val path = source_path.expand - if (dir == "" || path.is_absolute) + if (dir == "" || path.is_absolute) { MiscUtilities.resolveSymlinks(File.platform_path(path)) + } else if (path.is_current) dir else { val vfs = VFSManager.getVFSForPath(dir) - if (vfs.isInstanceOf[FileVFS]) + if (vfs.isInstanceOf[FileVFS]) { MiscUtilities.resolveSymlinks( vfs.constructPath(dir, File.platform_path(path))) + } else vfs.constructPath(dir, File.standard_path(path)) } } @@ -130,10 +132,12 @@ /* theory text edits */ override def commit(change: Session.Change): Unit = { - if (change.syntax_changed.nonEmpty) + if (change.syntax_changed.nonEmpty) { GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) } + } if (change.deps_changed || - PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version).nonEmpty) + PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version).nonEmpty) { PIDE.plugin.deps_changed() + } } }