tuned -- prefer immutable data;
authorwenzelm
Tue Sep 04 14:50:52 2018 +0200 (9 months ago)
changeset 6890590a6b714aca3
parent 68904 09151c54aaac
child 68906 a9deff1bcb65
tuned -- prefer immutable data;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:47:50 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:50:52 2018 +0200
     1.3 @@ -183,12 +183,12 @@
     1.4                      }
     1.5  
     1.6                      val progress_percentage =
     1.7 -                      for {
     1.8 +                      (for {
     1.9                          (name, node_status) <- nodes_status1.present.iterator
    1.10                          if changed.nodes.contains(name)
    1.11                          p1 = node_status.percentage
    1.12                          if p1 > 0 && Some(p1) != nodes_status.get(name).map(_.percentage)
    1.13 -                      } yield (name.theory, p1)
    1.14 +                      } yield (name.theory, p1)).toList
    1.15  
    1.16                      (progress_percentage, nodes_status1)
    1.17                    })