src/Pure/PIDE/command.scala

       if (markups1.is_empty) None
       else Some(State(other_command, markups = markups1))
     }
 
     private def add_status(st: Markup): State = {
-      val document_status1 =
-        document_status + Document_Status.Command_Status.make(markups = List(st))
+      val document_status1 = document_status.update(markups = List(st))
       new State(command, st :: status, results, exports, markups, document_status1)
     }
 
     private def add_result(entry: Results.Entry): State = {
       val document_status1 =