130 } |
130 } |
131 } |
131 } |
132 } |
132 } |
133 |
133 |
134 val results = { |
134 val results = { |
135 val build_results = |
135 val process_results = |
136 if (build_deps.is_empty) { |
136 Isabelle_Thread.uninterruptible { |
137 progress.echo_warning("Nothing to build") |
137 val build_process = |
138 Map.empty[String, Build_Process.Result] |
138 new Build_Process(build_context, build_heap = build_heap, |
139 } |
139 numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, |
140 else { |
140 no_build = no_build, verbose = verbose, session_setup = session_setup) |
141 Isabelle_Thread.uninterruptible { |
141 build_process.run() |
142 val build_process = |
|
143 new Build_Process(build_context, build_heap = build_heap, |
|
144 numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, |
|
145 no_build = no_build, verbose = verbose, session_setup = session_setup) |
|
146 build_process.run() |
|
147 } |
|
148 } |
142 } |
149 |
143 |
150 val sessions_ok: List[String] = |
144 val sessions_ok: List[String] = |
151 (for { |
145 (for { |
152 name <- build_deps.sessions_structure.build_topological_order.iterator |
146 name <- build_deps.sessions_structure.build_topological_order.iterator |
153 result <- build_results.get(name) |
147 result <- process_results.get(name) |
154 if result.ok |
148 if result.ok |
155 } yield name).toList |
149 } yield name).toList |
156 |
150 |
157 val results = |
151 new Results(store, build_deps, sessions_ok, process_results) |
158 (for ((name, result) <- build_results.iterator) |
|
159 yield (name, result.process_result)).toMap |
|
160 |
|
161 new Results(store, build_deps, sessions_ok, results) |
|
162 } |
152 } |
163 |
153 |
164 if (export_files) { |
154 if (export_files) { |
165 for (name <- full_sessions_selection.iterator if results(name).ok) { |
155 for (name <- full_sessions_selection.iterator if results(name).ok) { |
166 val info = results.info(name) |
156 val info = results.info(name) |