changeset 52642 | 84eb792224a8 |
parent 52536 | 3a35ce87a55c |
child 52849 | 199e9fa5a5c2 |
--- a/src/Pure/PIDE/command.scala Sat Jul 13 00:50:49 2013 +0200 +++ b/src/Pure/PIDE/command.scala Sat Jul 13 12:39:45 2013 +0200 @@ -130,7 +130,10 @@ } def ++ (other: State): State = - copy(results = results ++ other.results) // FIXME merge more content!? + copy( + status = other.status ::: status, + results = results ++ other.results, + markup = markup ++ other.markup) }