src/Pure/Thy/thy_resources.scala
changeset 68962 50676b0ab970
parent 68959 d4223afddd47
child 68981 30daac7848b9
equal deleted inserted replaced
68961:22a3790eecae 68962:50676b0ab970
   268 
   268 
   269                     val theory_progress =
   269                     val theory_progress =
   270                       (for {
   270                       (for {
   271                         (name, node_status) <- nodes_status1.present.iterator
   271                         (name, node_status) <- nodes_status1.present.iterator
   272                         if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
   272                         if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
   273                         percentage = Some(node_status.percentage)
   273                         p1 = node_status.percentage
   274                         if percentage != st.nodes_status.get(name).map(_.percentage)
   274                         if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
   275                       } yield Progress.Theory(name.theory, percentage = percentage)).toList
   275                       } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
   276 
   276 
   277                     (theory_progress, st.update(nodes_status1))
   277                     (theory_progress, st.update(nodes_status1))
   278                   })
   278                   })
   279 
   279 
   280               theory_progress.foreach(progress.theory(_))
   280               theory_progress.foreach(progress.theory(_))