src/Pure/PIDE/command.scala
changeset 83185 47edc6384e7a
parent 83184 9e05d3acd2b4
child 83186 887f1eac24d1
--- a/src/Pure/PIDE/command.scala	Wed Sep 17 11:30:59 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 17 11:41:27 2025 +0200
@@ -259,8 +259,7 @@
     }
 
     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)
     }