# HG changeset patch
# User wenzelm
# Date 1761559264 -3600
# Node ID b1a472adb667bd39d7b8d71ed14e5610035399b8
# Parent  182728f4e18beb2162a5368423bfdfe68d90330a
tuned;

diff -r 182728f4e18b -r b1a472adb667 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Mon Oct 27 10:33:53 2025 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Mon Oct 27 11:01:04 2025 +0100
@@ -73,8 +73,9 @@
           val results =
             List.from(
               for {
-                case (_, elem@XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
-                if props.contains((Markup.INSTANCE, state0.instance))
+                case (_, elem@XML.Elem(Markup(Markup.RESULT, props@Markup.Instance(instance)), _))
+                  <- command_results.iterator
+                if instance == state0.instance
               } yield elem)
           val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd)
           (snapshot, command_results, results, removed)