src/Pure/Build/build_job.scala
changeset 83221 f5143b09b192
parent 83215 0526a640f44f
child 83222 72e0b25a8f3c
equal deleted inserted replaced
83220:a6c91d4df0c6 83221:f5143b09b192
   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() }