# HG changeset patch
# User wenzelm
# Date 1536065452 -7200
# Node ID 90a6b714aca34978d993fd6e242358be76b469b2
# Parent  09151c54aaac6b40e6fb2a6dce8ad1298a927f5d
tuned -- prefer immutable data;

diff -r 09151c54aaac -r 90a6b714aca3 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)
                   })