diff -r b07735ce02b3 -r 4fe165254e20 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sun Sep 02 23:08:31 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sun Sep 02 23:25:53 2018 +0200
@@ -153,7 +153,7 @@
       val delay_nodes_status =
         Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
           val (nodes_status, names) = nodes_status_update.value
-          progress.nodes_status(names.map(name => (name -> nodes_status(name))))
+          progress.nodes_status(nodes_status, names)
         }
 
       val consumer =