equal
deleted
inserted
replaced
92 /* document node name */ |
92 /* document node name */ |
93 |
93 |
94 def node_file(name: Document.Node.Name): JFile = new JFile(name.node) |
94 def node_file(name: Document.Node.Name): JFile = new JFile(name.node) |
95 |
95 |
96 def node_name(file: JFile): Document.Node.Name = |
96 def node_name(file: JFile): Document.Node.Name = |
97 session_base.known.get_file(file, bootstrap = true) getOrElse { |
97 find_theory(Sessions.DRAFT, file) getOrElse { |
98 val node = file.getPath |
98 val node = file.getPath |
99 val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) |
99 val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) |
100 if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) |
100 if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) |
101 else { |
101 else { |
102 val master_dir = file.getParent |
102 val master_dir = file.getParent |