diff -r 22ad71030b46 -r 1a0857d96637 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Sat Oct 18 15:35:10 2025 +0200 +++ b/src/Pure/System/progress.scala Sat Oct 18 16:34:02 2025 +0200 @@ -141,12 +141,14 @@ override def nodes_status(nodes_status: Progress.Nodes_Status): Unit = synchronized { val old_status = status_clear() - - val session = nodes_status.session - val new_status = - (old_status.filterNot(p => p._1 == session) ::: - (if (status_detailed) nodes_status.status_theories.map((session, _)) else Nil)) - .sortBy(_._1) + val new_status = { + val buf = new mutable.ListBuffer[(String, Progress.Msg)] + val session = nodes_status.session + for (old <- old_status if old._1 < session) buf += old + if (status_detailed) { for (thy <- nodes_status.status_theories) buf += (session -> thy) } + for (old <- old_status if old._1 > session) buf += old + buf.toList + } output(nodes_status.completed_theories) output_status(new_status)