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) = |
73 def loaded_theory_name(qualifier: String, theory0: String): (Boolean, String) = |
74 session_base.loaded_theories.get(theory0) match { |
74 session_base.loaded_theories.get(theory0) match { |
75 case Some(theory) => (true, theory) |
75 case Some(theory) => (true, theory) |
76 case None => |
76 case None => |
77 val theory = |
77 val theory = |
78 if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) |
78 if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0) |
80 else Long_Name.qualify(qualifier, theory0) |
80 else Long_Name.qualify(qualifier, theory0) |
81 (false, theory) |
81 (false, theory) |
82 } |
82 } |
83 |
83 |
84 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 = |
85 { |
85 loaded_theory_name(qualifier, Thy_Header.import_name(s)) match { |
86 val (loaded, theory) = theory_name(qualifier, Thy_Header.import_name(s)) |
86 case (true, theory) => Document.Node.Name.loaded_theory(theory) |
87 if (loaded) Document.Node.Name.loaded_theory(theory) |
87 case (false, theory) => |
88 else |
88 session_base.known_theories.get(theory) match { |
89 session_base.known_theories.get(theory) match { |
89 case Some(node_name) => node_name |
90 case Some(node_name) => node_name |
90 case None => |
91 case None => |
91 val path = Path.explode(s) |
92 val path = Path.explode(s) |
92 val node = append(dir, thy_path(path)) |
93 val node = append(dir, thy_path(path)) |
93 val master_dir = append(dir, path.dir) |
94 val master_dir = append(dir, path.dir) |
94 Document.Node.Name(node, master_dir, theory) |
95 Document.Node.Name(node, master_dir, theory) |
95 } |
96 } |
96 } |
97 } |
|
98 |
97 |
99 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
98 def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
100 { |
99 { |
101 val path = Path.explode(name.node) |
100 val path = Path.explode(name.node) |
102 if (!path.is_file) error("No such file: " + path.toString) |
101 if (!path.is_file) error("No such file: " + path.toString) |