# HG changeset patch
# User wenzelm
# Date 1753800229 -7200
# Node ID eea4394dca0912d3c6eb934904c07eaee5492159
# Parent  77a3d85592880fa39bb159638deda208b3f8a598
tuned;

diff -r 77a3d8559288 -r eea4394dca09 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Jul 28 21:17:31 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Tue Jul 29 16:43:49 2025 +0200
@@ -120,13 +120,13 @@
         case Some(command) =>
           if (restriction.isEmpty || restriction.get.contains(command)) {
             val results = snapshot.command_results(command)
-
-            val (states, other) =
-              results.iterator.map(_._2).filterNot(Protocol.is_result).toList
-                .partition(Protocol.is_state)
-            val (urgent, regular) = other.partition(Protocol.is_urgent)
-            val messages = urgent ::: (if (output_state()) states else Nil) ::: regular
-
+            val messages = {
+              val (states, other) =
+                results.iterator.map(_._2).filterNot(Protocol.is_result).toList
+                  .partition(Protocol.is_state)
+              val (urgent, regular) = other.partition(Protocol.is_urgent)
+              urgent ::: (if (output_state()) states else Nil) ::: regular
+            }
             Editor.Output(results = results, messages = messages)
           }
           else Editor.Output.none