# HG changeset patch
# User wenzelm
# Date 1761745705 -3600
# Node ID 1ebb11300c088ddc610cd320079d7ba88ea47bdd
# Parent  e6c83fff076a2935305db2e7d3ba7031be50e2e2
clarified modules;

diff -r e6c83fff076a -r 1ebb11300c08 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Oct 29 14:08:10 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Oct 29 14:48:25 2025 +0100
@@ -249,6 +249,19 @@
   }
 
 
+  /* 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
+    }
+  }
+
+
   /* breakpoints */
 
   object ML_Breakpoint {
diff -r e6c83fff076a -r 1ebb11300c08 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Wed Oct 29 14:08:10 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Oct 29 14:48:25 2025 +0100
@@ -421,16 +421,6 @@
   /* code actions */
 
   def code_action_request(id: LSP.Id, file: JFile, range: Line.Range): Unit = {
-    def extract_sendbacks(body: XML.Body): List[(String, Properties.T)] = {
-      body match {
-        case XML.Elem(Markup(Markup.SENDBACK, props), b) :: rest =>
-          (XML.content(b), props) :: extract_sendbacks(rest)
-        case XML.Elem(_, b) :: rest => extract_sendbacks(b ::: rest)
-        case _ :: rest => extract_sendbacks(rest)
-        case Nil => Nil
-      }
-    }
-
     for {
       model <- resources.get_model(file)
       version <- model.version
@@ -443,7 +433,7 @@
           Text.Range(text_range.start - 1, text_range.stop + 1),
           Markup.Elements.full,
           command_states => _ => Some(command_states.flatMap(_.results.iterator.map(_._2).toList)))
-        .flatMap(info => extract_sendbacks(info.info).flatMap {
+        .flatMap(info => Protocol.senback_snippets(info.info).flatMap {
           (s, p) =>
             for {
               id <- Position.Id.unapply(p)