src/Pure/Thy/thy_resources.scala
changeset 68888 4fe165254e20
parent 68884 9b97d0b20d95
child 68894 1dbdad1b57a5
--- 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 =