23 |
23 |
24 class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base) |
24 class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base) |
25 { |
25 { |
26 /* document node name */ |
26 /* document node name */ |
27 |
27 |
|
28 def known_file(path: String): Option[Document.Node.Name] = |
|
29 JEdit_Lib.check_file(path).flatMap(session_base.known_file(_)) |
|
30 |
28 def node_name(path: String): Document.Node.Name = |
31 def node_name(path: String): Document.Node.Name = |
29 { |
32 known_file(path) getOrElse { |
30 val vfs = VFSManager.getVFSForPath(path) |
33 val vfs = VFSManager.getVFSForPath(path) |
31 val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path |
34 val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path |
32 theory_name(default_qualifier, Thy_Header.theory_name(node)) match { |
35 theory_name(default_qualifier, Thy_Header.theory_name(node)) match { |
33 case (true, theory) => Document.Node.Name.loaded_theory(theory) |
36 case (true, theory) => Document.Node.Name.loaded_theory(theory) |
34 case (false, theory) => |
37 case (false, theory) => |
35 val master_dir = if (theory == "") "" else vfs.getParentOfPath(path) |
38 val master_dir = if (theory == "") "" else vfs.getParentOfPath(path) |
36 Document.Node.Name(node, master_dir, theory) |
39 Document.Node.Name(node, master_dir, theory) |
|
40 } |
37 } |
41 } |
38 } |
|
39 |
42 |
40 def node_name(buffer: Buffer): Document.Node.Name = |
43 def node_name(buffer: Buffer): Document.Node.Name = |
41 node_name(JEdit_Lib.buffer_name(buffer)) |
44 node_name(JEdit_Lib.buffer_name(buffer)) |
42 |
45 |
43 def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = |
46 def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = |