# HG changeset patch
# User wenzelm
# Date 1761746639 -3600
# Node ID cb4f950f4fbdd58c924e0d1a8894103467f73c97
# Parent  1ebb11300c088ddc610cd320079d7ba88ea47bdd
more accurate senback_snippets: no duplicates, no recursion into "sendback" or wrapped elements;

diff -r 1ebb11300c08 -r cb4f950f4fbd src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Oct 29 14:48:25 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Oct 29 15:03:59 2025 +0100
@@ -6,6 +6,9 @@
 
 package isabelle
 
+import scala.collection.mutable
+import scala.annotation.tailrec
+
 
 object Protocol {
   /* markers for inlined messages */
@@ -251,14 +254,27 @@
 
   /* sendback snippets */
 
-  def senback_snippets(body: XML.Body): List[(String, Properties.T)] = {
-    body match {
-      case XML.Elem(Markup(Markup.SENDBACK, props), b) :: rest =>
-        (XML.content(b), props) :: senback_snippets(rest)
-      case XML.Elem(_, b) :: rest => senback_snippets(b ::: rest)
-      case _ :: rest => senback_snippets(rest)
-      case Nil => Nil
-    }
+  def senback_snippets(xml: XML.Body): List[(String, Properties.T)] = {
+    var seen = Set.empty[(String, Properties.T)]
+    val result = new mutable.ListBuffer[(String, Properties.T)]
+
+    @tailrec def traverse(body: XML.Body): Unit =
+      body match {
+        case XML.Elem(Markup(Markup.SENDBACK, props), body1) :: body2 =>
+          val entry = (XML.content(body1), props)
+          if (!seen(entry)) {
+            seen += entry
+            result += entry
+          }
+          traverse(body2)
+        case XML.Wrapped_Elem(_, _, body1) :: body2 => traverse(body1 ::: body2)
+        case XML.Elem(_, body1) :: body2 => traverse(body1 ::: body2)
+        case XML.Text(_) :: body2 => traverse(body2)
+        case Nil =>
+      }
+
+    traverse(xml)
+    result.toList
   }
 
 
diff -r 1ebb11300c08 -r cb4f950f4fbd src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Wed Oct 29 14:48:25 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Oct 29 15:03:59 2025 +0100
@@ -454,7 +454,7 @@
                   else current_text + s)
               (s, LSP.TextEdit(line_range, edit_text))
             }
-        }).distinct
+        })
 
       val actions = edits.map((name, edit) => {
         val text_edits = List(LSP.TextDocumentEdit(file, Some(version), List(edit)))