# HG changeset patch
# User wenzelm
# Date 1754233084 -7200
# Node ID 634b8a0f296659ae35997a08761d86cbb7b232d0
# Parent  37efc8611dca76b338da38f531bdfd85ae699ea6
more accurate range wrt. command chunk;

diff -r 37efc8611dca -r 634b8a0f2966 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Sun Aug 03 14:42:19 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Sun Aug 03 16:58:04 2025 +0200
@@ -125,8 +125,9 @@
       def filter(msg: XML.Elem): Boolean =
         (for {
           command_range <- thy_command_range
-          msg_offset <- Position.Offset.unapply(msg.markup.properties)
-        } yield command_range.contains(msg_offset)) getOrElse true
+          msg_range <- Position.Range.unapply(msg.markup.properties)
+          chunk_range <- thy_command.get.chunk.incorporate(msg_range)
+        } yield command_range.contains(chunk_range)) getOrElse true
 
       thy_command orElse snapshot.current_command(snapshot.node_name, offset) match {
         case None => Editor.Output.init