226 def nodes_status_progress(): Unit = { |
226 def nodes_status_progress(): Unit = { |
227 val state = session.get_state() |
227 val state = session.get_state() |
228 val result = |
228 val result = |
229 session.synchronized { |
229 session.synchronized { |
230 val nodes_status1 = |
230 val nodes_status1 = |
231 nodes_changed.foldLeft(nodes_status)( { case (status, state_id) => |
231 nodes_changed.foldLeft(nodes_status)({ case (status, state_id) => |
232 state.theory_snapshot(state_id, session.build_blobs) match { |
232 state.theory_snapshot(state_id, session.build_blobs) match { |
233 case None => status |
233 case None => status |
234 case Some(snapshot) => |
234 case Some(snapshot) => |
235 status.update_node(snapshot.state, snapshot.version, snapshot.node_name, |
235 status.update_node(snapshot.state, snapshot.version, snapshot.node_name, |
236 threshold = editor_timing_threshold) |
236 threshold = editor_timing_threshold) |
237 } |
237 } |
238 } |
238 }) |
239 ) |
239 val result = |
240 val changed = nodes_changed.nonEmpty |
240 if (nodes_changed.isEmpty) None |
|
241 else Some(Progress.Nodes_Status(nodes_domain, nodes_status1)) |
|
242 |
241 nodes_changed = Set.empty |
243 nodes_changed = Set.empty |
242 nodes_status = nodes_status1 |
244 nodes_status = nodes_status1 |
243 if (changed) Some(Progress.Nodes_Status(nodes_domain, nodes_status1)) else None |
245 |
|
246 result |
244 } |
247 } |
245 result.foreach(progress.nodes_status) |
248 result.foreach(progress.nodes_status) |
246 } |
249 } |
247 |
250 |
248 val nodes_delay = Delay.first(build_progress_delay) { nodes_status_progress() } |
251 val nodes_delay = Delay.first(build_progress_delay) { nodes_status_progress() } |