equal
deleted
inserted
replaced
33 def node_name(path: String): Document.Node.Name = |
33 def node_name(path: String): Document.Node.Name = |
34 JEdit_Lib.check_file(path).flatMap(find_theory) getOrElse { |
34 JEdit_Lib.check_file(path).flatMap(find_theory) getOrElse { |
35 val vfs = VFSManager.getVFSForPath(path) |
35 val vfs = VFSManager.getVFSForPath(path) |
36 val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path |
36 val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path |
37 val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) |
37 val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) |
38 if (session_base.loaded_theory(theory)) loaded_theory_node(theory) |
38 if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) |
39 else { |
39 else { |
40 val master_dir = vfs.getParentOfPath(path) |
40 val master_dir = vfs.getParentOfPath(path) |
41 Document.Node.Name(node, master_dir = master_dir, theory = theory) |
41 Document.Node.Name(node, master_dir = master_dir, theory = theory) |
42 } |
42 } |
43 } |
43 } |