equal
deleted
inserted
replaced
35 |
35 |
36 |
36 |
37 /* document node name */ |
37 /* document node name */ |
38 |
38 |
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(find_theory(_)) getOrElse { |
40 JEdit_Lib.check_file(path).flatMap(find_theory) 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)) loaded_theory_node(theory) |
44 if (session_base.loaded_theory(theory)) loaded_theory_node(theory) |
45 else { |
45 else { |