equal
deleted
inserted
replaced
70 def theory_qualifier(name: Document.Node.Name): String = |
70 def theory_qualifier(name: Document.Node.Name): String = |
71 Long_Name.qualifier(name.theory) |
71 Long_Name.qualifier(name.theory) |
72 |
72 |
73 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
73 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
74 { |
74 { |
75 val theory0 = Thy_Header.base_name(s) |
75 val theory0 = Thy_Header.import_name(s) |
76 val theory = |
76 val theory = |
77 if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0) |
77 if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0) |
78 || true /* FIXME */) theory0 |
78 || true /* FIXME */) theory0 |
79 else theory0 // FIXME Long_Name.qualify(qualifier, theory0) |
79 else theory0 // FIXME Long_Name.qualify(qualifier, theory0) |
80 |
80 |