--- a/src/Tools/VSCode/src/lsp.scala Sun Jun 30 15:22:36 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala Sun Jun 30 15:22:50 2024 +0200
@@ -341,8 +341,14 @@
object WorkspaceEdit {
def apply(edits: List[TextDocumentEdit]): JSON.T =
+ JSON.Object("documentChanges" -> edits.map(_.json))
+ }
+
+ object ApplyWorkspaceEdit {
+ def apply(edits: List[TextDocumentEdit]): JSON.T =
RequestMessage(Id.empty, "workspace/applyEdit",
- JSON.Object("edit" -> JSON.Object("documentChanges" -> edits.map(_.json))))
+ JSON.Object("edit" -> WorkspaceEdit(edits))
+ )
}