102 val declared_imports = |
102 val declared_imports = |
103 full_sessions.imports_ancestors(session_name).toSet + session_name |
103 full_sessions.imports_ancestors(session_name).toSet + session_name |
104 val extra_imports = |
104 val extra_imports = |
105 (for { |
105 (for { |
106 (_, a) <- session_resources.session_base.known.theories.iterator |
106 (_, a) <- session_resources.session_base.known.theories.iterator |
107 if session_resources.theory_qualifier(a) == info.theory_qualifier |
107 if session_resources.theory_qualifier(a) == info.name |
108 b <- deps.all_known.get_file(a.path.file) |
108 b <- deps.all_known.get_file(a.path.file) |
109 qualifier = session_resources.theory_qualifier(b) |
109 qualifier = session_resources.theory_qualifier(b) |
110 if !declared_imports.contains(qualifier) |
110 if !declared_imports.contains(qualifier) |
111 } yield qualifier).toSet |
111 } yield qualifier).toSet |
112 |
112 |
144 imports_resources.standard_import(session_resources, qualifier, dir, s) |
144 imports_resources.standard_import(session_resources, qualifier, dir, s) |
145 |
145 |
146 val updates_root = |
146 val updates_root = |
147 for { |
147 for { |
148 (_, pos) <- info.theories.flatMap(_._2) |
148 (_, pos) <- info.theories.flatMap(_._2) |
149 upd <- update_name(root_keywords, pos, |
149 upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _)) |
150 standard_import(info.theory_qualifier, info.dir.implode, _)) |
|
151 } yield upd |
150 } yield upd |
152 |
151 |
153 val updates_theories = |
152 val updates_theories = |
154 for { |
153 for { |
155 (_, name) <- session_base.known.theories_local.toList |
154 (_, name) <- session_base.known.theories_local.toList |
156 if session_resources.theory_qualifier(name) == info.theory_qualifier |
155 if session_resources.theory_qualifier(name) == info.name |
157 (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports |
156 (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports |
158 upd <- update_name(session_base.overall_syntax.keywords, pos, |
157 upd <- update_name(session_base.overall_syntax.keywords, pos, |
159 standard_import(session_resources.theory_qualifier(name), name.master_dir, _)) |
158 standard_import(session_resources.theory_qualifier(name), name.master_dir, _)) |
160 } yield upd |
159 } yield upd |
161 |
160 |