equal
deleted
inserted
replaced
57 |
57 |
58 val empty: Command_Status = make(Iterator.empty) |
58 val empty: Command_Status = make(Iterator.empty) |
59 |
59 |
60 def merge(status_iterator: Iterator[Command_Status]): Command_Status = |
60 def merge(status_iterator: Iterator[Command_Status]): Command_Status = |
61 if (status_iterator.hasNext) { |
61 if (status_iterator.hasNext) { |
62 val status0 = status_iterator.next |
62 val status0 = status_iterator.next() |
63 (status0 /: status_iterator)(_ + _) |
63 (status0 /: status_iterator)(_ + _) |
64 } |
64 } |
65 else empty |
65 else empty |
66 } |
66 } |
67 |
67 |