--- a/src/Pure/PIDE/protocol.scala Sat Jan 14 15:20:29 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Sat Jan 14 15:30:54 2012 +0100
@@ -41,7 +41,7 @@
}
- /* toplevel transactions */
+ /* command status */
sealed case class Status(
private val finished: Boolean = false,
@@ -70,6 +70,9 @@
def command_status(markups: List[Markup]): Status =
(Status() /: markups)(command_status(_, _))
+
+ /* node status */
+
sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
{
def total: Int = unprocessed + running + finished + failed