changeset 44866 | 0eb8284a64bd |
parent 44676 | 7de87f1ae965 |
child 44979 | 68b990e950b1 |
--- a/src/Pure/PIDE/isar_document.scala Sat Sep 10 16:30:08 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Sat Sep 10 20:22:22 2011 +0200 @@ -63,6 +63,9 @@ } sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) + { + def total: Int = unprocessed + running + finished + failed + } def node_status( state: Document.State, version: Document.Version, node: Document.Node): Node_Status =