lsp: clarified WorkspaceEdit;
authorThomas Lindae <thomas.lindae@in.tum.de>
Sun, 30 Jun 2024 15:22:50 +0200
changeset 81066 18c98588388d
parent 81065 37590e377db6
child 81067 1b1d72c45ff4
lsp: clarified WorkspaceEdit;
src/Tools/VSCode/src/lsp.scala
--- 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))
+      )
   }