src/Pure/System/progress.scala
changeset 83309 1a0857d96637
parent 83306 2616fa68b9c6
child 83315 03dfb684a50d
--- 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)