equal
deleted
inserted
replaced
61 else if (markup.exists(_.name == Markup.FINISHED)) Finished |
61 else if (markup.exists(_.name == Markup.FINISHED)) Finished |
62 else Unprocessed |
62 else Unprocessed |
63 } |
63 } |
64 |
64 |
65 sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) |
65 sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) |
|
66 { |
|
67 def total: Int = unprocessed + running + finished + failed |
|
68 } |
66 |
69 |
67 def node_status( |
70 def node_status( |
68 state: Document.State, version: Document.Version, node: Document.Node): Node_Status = |
71 state: Document.State, version: Document.Version, node: Document.Node): Node_Status = |
69 { |
72 { |
70 var unprocessed = 0 |
73 var unprocessed = 0 |