| changeset 50540 | f4aac67a6405 |
| parent 50508 | 5b7150395568 |
| child 51048 | 123be08eed88 |
| 50539:3b68e5760a2d | 50540:f4aac67a6405 |
|---|---|
37 |
37 |
38 def ++ (other: Results): Results = |
38 def ++ (other: Results): Results = |
39 if (this eq other) this |
39 if (this eq other) this |
40 else if (rep.isEmpty) other |
40 else if (rep.isEmpty) other |
41 else (this /: other.entries)(_ + _) |
41 else (this /: other.entries)(_ + _) |
42 |
|
43 override def toString: String = entries.mkString("Results(", ", ", ")") |
|
42 } |
44 } |
43 |
45 |
44 |
46 |
45 /* state */ |
47 /* state */ |
46 |
48 |