68 else Nil |
68 else Nil |
69 |
69 |
70 def theory_qualifier(name: Document.Node.Name): String = |
70 def theory_qualifier(name: Document.Node.Name): String = |
71 session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory)) |
71 session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory)) |
72 |
72 |
|
73 def theory_name(qualifier: String, theory0: String): (Boolean, String) = |
|
74 session_base.loaded_theories.get(theory0) match { |
|
75 case Some(theory) => (true, theory) |
|
76 case None => |
|
77 val theory = |
|
78 if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) |
|
79 || true /* FIXME */) theory0 |
|
80 else Long_Name.qualify(qualifier, theory0) |
|
81 (false, theory) |
|
82 } |
|
83 |
73 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
84 def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
74 { |
85 { |
75 val theory0 = Thy_Header.import_name(s) |
86 val (loaded, theory) = theory_name(qualifier, Thy_Header.import_name(s)) |
76 val theory = |
87 if (loaded) Document.Node.Name.loaded_theory(theory) |
77 if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) |
88 else |
78 || true /* FIXME */) theory0 |
89 session_base.known_theories.get(theory) match { |
79 else Long_Name.qualify(qualifier, theory0) |
90 case Some(node_name) => node_name |
80 |
91 case None => |
81 session_base.loaded_theories.get(theory) orElse |
92 val path = Path.explode(s) |
82 session_base.loaded_theories.get(theory0) orElse |
93 val node = append(dir, thy_path(path)) |
83 session_base.known_theories.get(theory) orElse |
94 val master_dir = append(dir, path.dir) |
84 session_base.known_theories.get(theory0) getOrElse { |
95 Document.Node.Name(node, master_dir, theory) |
85 val path = Path.explode(s) |
96 } |
86 val node = append(dir, thy_path(path)) |
|
87 val master_dir = append(dir, path.dir) |
|
88 Document.Node.Name(node, master_dir, theory) |
|
89 } |
|
90 } |
97 } |
91 |
98 |
92 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
99 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
93 { |
100 { |
94 val path = Path.explode(name.node) |
101 val path = Path.explode(name.node) |