--- 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 {
--- 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)