equal
deleted
inserted
replaced
89 /* document node name */ |
89 /* document node name */ |
90 |
90 |
91 def node_file(name: Document.Node.Name): JFile = new JFile(name.node) |
91 def node_file(name: Document.Node.Name): JFile = new JFile(name.node) |
92 |
92 |
93 def node_name(file: JFile): Document.Node.Name = |
93 def node_name(file: JFile): Document.Node.Name = |
94 thy_node_name(Sessions.DRAFT, file, bootstrap = true) |
94 session_base.known.get_file(file, bootstrap = true) getOrElse { |
|
95 val node = file.getPath |
|
96 theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match { |
|
97 case (true, theory) => Document.Node.Name.loaded_theory(theory) |
|
98 case (false, theory) => |
|
99 val master_dir = if (theory == "") "" else file.getParent |
|
100 Document.Node.Name(node, master_dir, theory) |
|
101 } |
|
102 } |
95 |
103 |
96 override def append(dir: String, source_path: Path): String = |
104 override def append(dir: String, source_path: Path): String = |
97 { |
105 { |
98 val path = source_path.expand |
106 val path = source_path.expand |
99 if (dir == "" || path.is_absolute) File.platform_path(path) |
107 if (dir == "" || path.is_absolute) File.platform_path(path) |