tuned;
authorwenzelm
Wed, 29 Oct 2025 14:08:10 +0100
changeset 83426 e6c83fff076a
parent 83425 aa11710730c9
child 83427 1ebb11300c08
tuned;
src/Tools/VSCode/src/language_server.scala
--- 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
       }
     }