src/Pure/PIDE/protocol.scala
changeset 68321 daca5f2a0c90
parent 67923 3e072441c96a
child 68323 bf7336731981
--- a/src/Pure/PIDE/protocol.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue May 29 20:00:10 2018 +0200
@@ -156,9 +156,10 @@
   def node_status(
     state: Document.State,
     version: Document.Version,
-    name: Document.Node.Name,
-    node: Document.Node): Node_Status =
+    name: Document.Node.Name): Node_Status =
   {
+    val node = version.nodes(name)
+
     var unprocessed = 0
     var running = 0
     var warned = 0