152 import_name(session_base.theory_qualifier(name), name.master_dir, s) |
152 import_name(session_base.theory_qualifier(name), name.master_dir, s) |
153 |
153 |
154 def import_name(info: Sessions.Info, s: String): Document.Node.Name = |
154 def import_name(info: Sessions.Info, s: String): Document.Node.Name = |
155 import_name(info.name, info.dir.implode, s) |
155 import_name(info.name, info.dir.implode, s) |
156 |
156 |
157 def find_theory(default_qualifier: String, file: JFile): Option[Document.Node.Name] = |
157 def find_theory(file: JFile): Option[Document.Node.Name] = |
158 { |
158 { |
159 val dir = File.canonical(file).getParentFile |
159 for { |
160 val qualifier = session_base.session_directories.get(dir).getOrElse(default_qualifier) |
160 qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile) |
161 Thy_Header.theory_name(file.getName) match { |
161 theory_base <- proper_string(Thy_Header.theory_name(file.getName)) |
162 case "" => None |
162 theory = theory_name(qualifier, theory_base) |
163 case s => Some(import_name(qualifier, File.path(file).dir.implode, s)) |
163 theory_node <- find_theory_node(theory) |
164 } |
164 if File.eq(theory_node.path.file, file) |
|
165 } yield theory_node |
165 } |
166 } |
166 |
167 |
167 def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] = |
168 def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] = |
168 (for { |
169 (for { |
169 (options, thys) <- info.theories.iterator |
170 (options, thys) <- info.theories.iterator |