# HG changeset patch
# User wenzelm
# Date 1753883411 -7200
# Node ID 471a1f2844379b83ea00863a4b4a77955bacb1d9
# Parent  0fcbdb9071382fbb005669a79c31cee8afd6c0d4
minor performance tuning;

diff -r 0fcbdb907138 -r 471a1f284437 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Wed Jul 30 13:56:41 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Wed Jul 30 15:50:11 2025 +0200
@@ -125,8 +125,8 @@
       def filter(msg: XML.Elem): Boolean =
         (for {
           command_range <- thy_command_range
-          range <- Position.Range.unapply(msg.markup.properties)
-        } yield command_range.contains(range)) getOrElse true
+          msg_offset <- Position.Offset.unapply(msg.markup.properties)
+        } yield command_range.contains(msg_offset)) getOrElse true
 
       thy_command orElse snapshot.current_command(snapshot.node_name, offset) match {
         case None => Editor.Output.init