# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719753756 -7200
# Node ID 37590e377db68aa7d91672f1461e63192abcae8e
# Parent  e81864b37183992bb510078c4908b93b852ec69b
lsp: made TextDocumentEdit accept optional versions;

diff -r e81864b37183 -r 37590e377db6 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sun Jun 30 15:32:51 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Jun 30 15:22:36 2024 +0200
@@ -328,11 +328,15 @@
     def json: JSON.T = JSON.Object("range" -> Range(range), "newText" -> new_text)
   }
 
-  sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit]) {
+  sealed case class TextDocumentEdit(file: JFile, version: Option[Long], edits: List[TextEdit]) {
     def json: JSON.T =
       JSON.Object(
-        "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version),
-        "edits" -> edits.map(_.json))
+        "textDocument" -> (
+          JSON.Object("uri" -> Url.print_file(file)) ++
+          JSON.optional("version" -> version)
+        ),
+        "edits" -> edits.map(_.json)
+      )
   }
 
   object WorkspaceEdit {