--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 17 21:26:23 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 17 21:48:53 2017 +0200
@@ -25,17 +25,20 @@
{
/* document node name */
+ def known_file(path: String): Option[Document.Node.Name] =
+ JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
+
def node_name(path: String): Document.Node.Name =
- {
- val vfs = VFSManager.getVFSForPath(path)
- val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
- theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
- case (true, theory) => Document.Node.Name.loaded_theory(theory)
- case (false, theory) =>
- val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
- Document.Node.Name(node, master_dir, theory)
+ known_file(path) getOrElse {
+ val vfs = VFSManager.getVFSForPath(path)
+ val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
+ theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+ case (true, theory) => Document.Node.Name.loaded_theory(theory)
+ case (false, theory) =>
+ val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
+ Document.Node.Name(node, master_dir, theory)
+ }
}
- }
def node_name(buffer: Buffer): Document.Node.Name =
node_name(JEdit_Lib.buffer_name(buffer))