# HG changeset patch
# User wenzelm
# Date 1535923553 -7200
# Node ID 4fe165254e20f07c19588b9a0e155f6497779804
# Parent  b07735ce02b317edea06ab1a19639c63c071912d
clarified signature;

diff -r b07735ce02b3 -r 4fe165254e20 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun Sep 02 23:08:31 2018 +0200
+++ b/src/Pure/System/progress.scala	Sun Sep 02 23:25:53 2018 +0200
@@ -21,7 +21,7 @@
   def echo(msg: String) {}
   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
   def theory(session: String, theory: String) {}
-  def nodes_status(nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)]) {}
+  def nodes_status(nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name]) {}
 
   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
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 =
diff -r b07735ce02b3 -r 4fe165254e20 src/Pure/Tools/server.scala
--- 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))
     }