changeset 68904 | 09151c54aaac |
parent 68903 | 58525b08eed1 |
child 68957 | eef4e983fd9d |
--- a/src/Pure/Tools/server.scala Tue Sep 04 14:40:31 2018 +0200 +++ b/src/Pure/Tools/server.scala Tue Sep 04 14:47:50 2018 +0200 @@ -276,7 +276,7 @@ override def nodes_status(nodes_status: Document_Status.Nodes_Status) { val json = - for ((name, node_status) <- nodes_status.dest) + for ((name, node_status) <- nodes_status.present) yield name.json + ("status" -> nodes_status(name).json) context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json)) }