67 } |
67 } |
68 else Nil |
68 else Nil |
69 |
69 |
70 def import_name(dir: String, s: String): Document.Node.Name = |
70 def import_name(dir: String, s: String): Document.Node.Name = |
71 { |
71 { |
72 val thy = Thy_Header.base_name(s) |
72 val theory0 = Thy_Header.base_name(s) |
73 val is_global = session_base.global_theories.contains(thy) |
73 val theory = |
74 val is_qualified = Long_Name.is_qualified(thy) |
74 if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0 |
|
75 else Long_Name.qualify(session_name, theory0) |
75 |
76 |
76 val known_theory = |
77 session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match |
77 session_base.known_theories.get(thy) orElse |
78 { |
78 (if (is_global) None |
|
79 else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy)) |
|
80 else session_base.known_theories.get(Long_Name.qualify(session_name, thy))) |
|
81 |
|
82 known_theory match { |
|
83 case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory) |
79 case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory) |
84 case Some(name) => name |
80 case Some(name) => name |
85 case None => |
81 case None => |
86 val path = Path.explode(s) |
82 val path = Path.explode(s) |
87 val node = append(dir, thy_path(path)) |
83 val node = append(dir, thy_path(path)) |
88 val master_dir = append(dir, path.dir) |
84 val master_dir = append(dir, path.dir) |
89 val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy) |
|
90 Document.Node.Name(node, master_dir, theory) |
85 Document.Node.Name(node, master_dir, theory) |
91 } |
86 } |
92 } |
87 } |
93 |
88 |
94 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
89 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |