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