98 dirs: List[Path] = Nil, |
98 dirs: List[Path] = Nil, |
99 select_dirs: List[Path] = Nil, |
99 select_dirs: List[Path] = Nil, |
100 verbose: Boolean = false) = |
100 verbose: Boolean = false) = |
101 { |
101 { |
102 val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs) |
102 val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs) |
103 val selected_sessions = full_sessions.selection(selection) |
|
104 |
103 |
105 val deps = |
104 val deps = |
106 Sessions.deps(selected_sessions, full_sessions.global_theories, |
105 Sessions.deps(full_sessions.selection(selection), full_sessions.global_theories, |
107 progress = progress, verbose = verbose).check_errors |
106 progress = progress, verbose = verbose).check_errors |
108 |
107 |
109 val root_keywords = Sessions.root_syntax.keywords |
108 val root_keywords = Sessions.root_syntax.keywords |
110 |
109 |
111 if (operation_imports) { |
110 if (operation_imports) { |
112 val report_imports: List[Report] = |
111 val report_imports: List[Report] = |
113 selected_sessions.build_topological_order.map((session_name: String) => |
112 deps.sessions_structure.build_topological_order.map((session_name: String) => |
114 { |
113 { |
115 val info = selected_sessions(session_name) |
114 val info = deps.sessions_structure(session_name) |
116 val session_base = deps(session_name) |
115 val session_base = deps(session_name) |
117 |
116 |
118 val declared_imports = |
117 val declared_imports = |
119 selected_sessions.imports_requirements(List(session_name)).toSet |
118 deps.sessions_structure.imports_requirements(List(session_name)).toSet |
120 |
119 |
121 val extra_imports = |
120 val extra_imports = |
122 (for { |
121 (for { |
123 (_, a) <- session_base.known.theories.iterator |
122 (_, a) <- session_base.known.theories.iterator |
124 if session_base.theory_qualifier(a) == info.name |
123 if session_base.theory_qualifier(a) == info.name |
126 qualifier = session_base.theory_qualifier(b) |
125 qualifier = session_base.theory_qualifier(b) |
127 if !declared_imports.contains(qualifier) |
126 if !declared_imports.contains(qualifier) |
128 } yield qualifier).toSet |
127 } yield qualifier).toSet |
129 |
128 |
130 val loaded_imports = |
129 val loaded_imports = |
131 selected_sessions.imports_requirements( |
130 deps.sessions_structure.imports_requirements( |
132 session_base.loaded_theories.keys.map(a => |
131 session_base.loaded_theories.keys.map(a => |
133 session_base.theory_qualifier(session_base.known.theories(a)))) |
132 session_base.theory_qualifier(session_base.known.theories(a)))) |
134 .toSet - session_name |
133 .toSet - session_name |
135 |
134 |
136 val minimal_imports = |
135 val minimal_imports = |
137 loaded_imports.filter(s1 => |
136 loaded_imports.filter(s1 => |
138 !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2))) |
137 !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2))) |
139 |
138 |
140 def make_result(set: Set[String]): Option[List[String]] = |
139 def make_result(set: Set[String]): Option[List[String]] = |
141 if (set.isEmpty) None |
140 if (set.isEmpty) None |
142 else Some(selected_sessions.imports_topological_order.filter(set)) |
141 else Some(deps.sessions_structure.imports_topological_order.filter(set)) |
143 |
142 |
144 Report(info, declared_imports, make_result(extra_imports), |
143 Report(info, declared_imports, make_result(extra_imports), |
145 if (loaded_imports == declared_imports - session_name) None |
144 if (loaded_imports == declared_imports - session_name) None |
146 else make_result(minimal_imports)) |
145 else make_result(minimal_imports)) |
147 }) |
146 }) |
171 } |
170 } |
172 |
171 |
173 if (operation_update) { |
172 if (operation_update) { |
174 progress.echo("\nUpdate theory imports" + update_message + ":") |
173 progress.echo("\nUpdate theory imports" + update_message + ":") |
175 val updates = |
174 val updates = |
176 selected_sessions.build_topological_order.flatMap(session_name => |
175 deps.sessions_structure.build_topological_order.flatMap(session_name => |
177 { |
176 { |
178 val info = selected_sessions(session_name) |
177 val info = deps.sessions_structure(session_name) |
179 val session_base = deps(session_name) |
178 val session_base = deps(session_name) |
180 val session_resources = new Resources(session_base) |
179 val session_resources = new Resources(session_base) |
181 val imports_base = session_base.get_imports |
180 val imports_base = session_base.get_imports |
182 val imports_resources = new Resources(imports_base) |
181 val imports_resources = new Resources(imports_base) |
183 |
182 |