equal
deleted
inserted
replaced
39 def node_name(path: String): Document.Node.Name = |
39 def node_name(path: String): Document.Node.Name = |
40 JEdit_Lib.check_file(path).flatMap(file => find_theory(Sessions.DRAFT, file)) getOrElse { |
40 JEdit_Lib.check_file(path).flatMap(file => find_theory(Sessions.DRAFT, file)) getOrElse { |
41 val vfs = VFSManager.getVFSForPath(path) |
41 val vfs = VFSManager.getVFSForPath(path) |
42 val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path |
42 val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path |
43 val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) |
43 val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) |
44 if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) |
44 if (session_base.loaded_theory(theory)) loaded_theory_node(theory) |
45 else { |
45 else { |
46 val master_dir = vfs.getParentOfPath(path) |
46 val master_dir = vfs.getParentOfPath(path) |
47 Document.Node.Name(node, master_dir, theory) |
47 Document.Node.Name(node, master_dir, theory) |
48 } |
48 } |
49 } |
49 } |