src/Pure/PIDE/command.scala
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)
   }