src/Pure/Tools/server.scala
changeset 68770 add44e2b8cb0
parent 68530 a110dcc9a4c7
child 68888 4fe165254e20
--- a/src/Pure/Tools/server.scala	Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Pure/Tools/server.scala	Sat Aug 18 22:09:09 2018 +0200
@@ -268,10 +268,20 @@
     override def echo(msg: String): Unit = context.writeln(msg, more:_*)
     override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
     override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
+
     override def theory(session: String, theory: String): Unit =
       context.writeln(Progress.theory_message(session, theory),
         (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
 
+    override def nodes_status(
+      nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)])
+    {
+      val json =
+        for ((name, status) <- nodes_status)
+        yield name.json + ("status" -> status.json)
+      context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
+    }
+
     @volatile private var is_stopped = false
     override def stopped: Boolean = is_stopped
     def stop { is_stopped = true }