equal
deleted
inserted
replaced
134 } |
134 } |
135 |
135 |
136 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
136 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
137 { |
137 { |
138 val theory = theory_name(qualifier, Thy_Header.import_name(s)) |
138 val theory = theory_name(qualifier, Thy_Header.import_name(s)) |
139 if (session_base.loaded_theory(theory)) loaded_theory_node(theory) |
139 def theory_node = make_theory_node(dir, thy_path(Path.explode(s)), theory) |
|
140 |
|
141 if (!Thy_Header.is_base_name(s)) theory_node |
|
142 else if (session_base.loaded_theory(theory)) loaded_theory_node(theory) |
140 else { |
143 else { |
141 find_theory_node(theory) match { |
144 find_theory_node(theory) match { |
142 case Some(node_name) => node_name |
145 case Some(node_name) => node_name |
143 case None => |
146 case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node |
144 if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)) |
|
145 loaded_theory_node(theory) |
|
146 else make_theory_node(dir, thy_path(Path.explode(s)), theory) |
|
147 } |
147 } |
148 } |
148 } |
149 } |
149 } |
150 |
150 |
151 def import_name(name: Document.Node.Name, s: String): Document.Node.Name = |
151 def import_name(name: Document.Node.Name, s: String): Document.Node.Name = |