equal
deleted
inserted
replaced
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 loaded_theory_name(qualifier: String, theory0: String): (Boolean, String) = |
73 def 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 loaded_theory_name(qualifier, Thy_Header.import_name(s)) match { |
85 theory_name(qualifier, Thy_Header.import_name(s)) match { |
86 case (true, theory) => Document.Node.Name.loaded_theory(theory) |
86 case (true, theory) => Document.Node.Name.loaded_theory(theory) |
87 case (false, theory) => |
87 case (false, theory) => |
88 session_base.known_theories.get(theory) match { |
88 session_base.known_theories.get(theory) match { |
89 case Some(node_name) => node_name |
89 case Some(node_name) => node_name |
90 case None => |
90 case None => |