src/Pure/PIDE/protocol.scala
changeset 67883 171e7735ce25
parent 67493 c4e9e0c50487
child 67915 d827728b74b3
     1.1 --- a/src/Pure/PIDE/protocol.scala	Fri Mar 16 17:16:09 2018 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Mar 16 18:42:35 2018 +0100
     1.3 @@ -146,6 +146,11 @@
     1.4    {
     1.5      def total: Int = unprocessed + running + warned + failed + finished
     1.6      def ok: Boolean = failed == 0
     1.7 +
     1.8 +    def json: JSON.Object.T =
     1.9 +      JSON.Object("unprocessed" -> unprocessed, "running" -> running, "warned" -> warned,
    1.10 +        "failed" -> failed, "finished" -> finished, "consolidated" -> consolidated,
    1.11 +        "total" -> total, "ok" -> ok)
    1.12    }
    1.13  
    1.14    def node_status(