| 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) }