# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719753770 -7200
# Node ID 18c98588388d44fadc69b31546b280dc3447ca8d
# Parent  37590e377db68aa7d91672f1461e63192abcae8e
lsp: clarified WorkspaceEdit;

diff -r 37590e377db6 -r 18c98588388d 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))
+      )
   }