src/Pure/PIDE/isar_document.scala
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 =