tuned -- prefer immutable data;
authorwenzelm
Tue, 04 Sep 2018 14:50:52 +0200
changeset 68905 90a6b714aca3
parent 68904 09151c54aaac
child 68906 a9deff1bcb65
tuned -- prefer immutable data;
src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:47:50 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:50:52 2018 +0200
@@ -183,12 +183,12 @@
                     }
 
                     val progress_percentage =
-                      for {
+                      (for {
                         (name, node_status) <- nodes_status1.present.iterator
                         if changed.nodes.contains(name)
                         p1 = node_status.percentage
                         if p1 > 0 && Some(p1) != nodes_status.get(name).map(_.percentage)
-                      } yield (name.theory, p1)
+                      } yield (name.theory, p1)).toList
 
                     (progress_percentage, nodes_status1)
                   })