--- a/src/Tools/VSCode/src/language_server.scala Wed Oct 29 14:07:56 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Wed Oct 29 14:08:10 2025 +0100
@@ -423,10 +423,10 @@
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, p), b) :: rest =>
- (XML.content(b), p) :: extract_sendbacks(rest)
- case XML.Elem(m, b) :: rest => extract_sendbacks(b ++ rest)
- case e :: rest => extract_sendbacks(rest)
+ 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
}
}