src/Pure/Tools/server.scala
changeset 68888 4fe165254e20
parent 68770 add44e2b8cb0
child 68903 58525b08eed1
--- a/src/Pure/Tools/server.scala	Sun Sep 02 23:08:31 2018 +0200
+++ b/src/Pure/Tools/server.scala	Sun Sep 02 23:25:53 2018 +0200
@@ -274,11 +274,9 @@
         (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
 
     override def nodes_status(
-      nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)])
+      nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name])
     {
-      val json =
-        for ((name, status) <- nodes_status)
-        yield name.json + ("status" -> status.json)
+      val json = names.map(name => name.json + ("status" -> nodes_status(name).json))
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }