fix: include non-optional version in VersionedTextDocumentIdentifier json

script/benchReelabRss.lean

@@ -56,8 +56,8 @@ def main (args : List String) : IO Unit := do
         versionNo := versionNo + 1
         let params : DidChangeTextDocumentParams := {
           textDocument := {
-            uri      := uri
-            version? := versionNo
+            uri     := uri
+            version := versionNo
           }
           contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
             start := headerEndPos

script/benchReelabWatchdogRss.lean

@@ -53,8 +53,8 @@ def main (args : List String) : IO Unit := do
         versionNo := versionNo + 1
         let params : DidChangeTextDocumentParams := {
           textDocument := {
-            uri      := uri
-            version? := versionNo
+            uri     := uri
+            version := versionNo
           }
           contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
             start := headerEndPos

src/Lean/Data/Lsp/Basic.lean

@@ -142,12 +142,23 @@ structure TextDocumentIdentifier where
   uri : DocumentUri
   deriving ToJson, FromJson
 
+/--
+Identifies a text document, and optionally specifies a specific version of the document. Used both
+for LSP's `VersionedTextDocumentIdentifier`, whose `version` is always present, and for its
+`OptionalVersionedTextDocumentIdentifier` (e.g. in `TextDocumentEdit`), whose `version` is `null`
+when it is not known (for instance, because the document is not open in the editor or does not yet
+exist).
+
+[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#optionalVersionedTextDocumentIdentifier)
+-/
 structure VersionedTextDocumentIdentifier where
   uri : DocumentUri
-  version? : Option Nat := none
+  /-- The version of the document, if known. Serialized as `"version": null` when `none` (hence no
+  `?` in the field name), since `OptionalVersionedTextDocumentIdentifier` requires the field. -/
+  version : Option Nat := none
   deriving ToJson, FromJson
 
-/-- A batch of `TextEdit`s to perform on a versioned text document.
+/-- A batch of `TextEdit`s to perform on an optionally versioned text document.
 
 [reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocumentEdit) -/
 structure TextDocumentEdit where

src/Lean/Server/FileWorker.lean

@@ -512,7 +512,7 @@ section Initialization
             params.version?
           | some (.notification "$/lean/fileProgress" (some params)) =>
             let params : LeanFileProgressParams ← fromJson? (toJson params) |>.toOption
-            params.textDocument.version?
+            params.textDocument.version
           | some (.notification "$/lean/ileanInfoUpdate" (some params))
           | some (.notification "$/lean/ileanInfoFinal" (some params)) =>
             let params : LeanIleanInfoParams ← fromJson? (toJson params) |>.toOption
@@ -587,7 +587,7 @@ section NotificationHandling
     let st ← get
     let oldDoc := (←get).doc
     let cancelTk ← RequestCancellationToken.new
-    let newVersion := docId.version?.getD 0
+    let newVersion := docId.version.getD 0
     let rc : RequestContext := {
       rpcSessions := st.rpcSessions
       doc := oldDoc

src/Lean/Server/FileWorker/Utils.lean

@@ -174,7 +174,7 @@ namespace EditableDocument
 /-- Construct a VersionedTextDocumentIdentifier from an EditableDocument --/
 def versionedIdentifier (ed : EditableDocument) : Lsp.VersionedTextDocumentIdentifier := {
   uri := ed.meta.uri
-  version? := some ed.meta.version
+  version := some ed.meta.version
 }
 
 end EditableDocument

src/Lean/Server/Test/Runner.lean

@@ -449,8 +449,8 @@ def processEdit : RunnerM Unit := do
     | throw <| IO.userError s!"failed to parse {insert}"
   let params : DidChangeTextDocumentParams := {
     textDocument := {
-      uri      := s.uri
-      version? := s.versionNo
+      uri     := s.uri
+      version := s.versionNo
     }
     contentChanges := #[
       TextDocumentContentChangeEvent.rangeChange {

src/Lean/Server/Utils.lean

@@ -151,7 +151,7 @@ def mkFileProgressNotification (m : DocumentMeta) (processing : Array LeanFilePr
     JsonRpc.Notification Lsp.LeanFileProgressParams where
   method := "$/lean/fileProgress"
   param := {
-    textDocument := { uri := m.uri, version? := m.version }
+    textDocument := { uri := m.uri, version := m.version }
     processing
   }
 

src/Lean/Server/Watchdog.lean

@@ -1247,7 +1247,7 @@ section NotificationHandling
       -- Global search and replace in VS Code will send `didChange` to files that were never opened.
       | return
     let oldDoc := fw.doc
-    let newVersion := doc.version?.getD 0
+    let newVersion := doc.version.getD 0
     if changes.isEmpty then
       return
     let newDocText := foldDocumentChanges changes oldDoc.text

tests/elab/lspOptionalVersion.lean

@@ -0,0 +1,56 @@
+import Lean.Data.Lsp.Basic
+
+open Lean Lsp
+
+/-!
+`VersionedTextDocumentIdentifier` serializes `version := none` as `"version": null`, since LSP's
+`OptionalVersionedTextDocumentIdentifier` requires the field.
+-/
+
+/-- info: {"version": null, "uri": "file:///a.lean"} -/
+#guard_msgs in
+#eval toJson ({ uri := "file:///a.lean" } : VersionedTextDocumentIdentifier)
+
+/-- info: {"version": 3, "uri": "file:///a.lean"} -/
+#guard_msgs in
+#eval toJson ({ uri := "file:///a.lean", version := some 3 } : VersionedTextDocumentIdentifier)
+
+/-! A `TextDocumentEdit` for a document whose version is unknown, e.g. one being created. -/
+
+/--
+info: {"documentChanges":
+ [{"textDocument": {"version": null, "uri": "file:///a.lean"},
+   "edits":
+   [{"range":
+     {"start": {"line": 0, "character": 0}, "end": {"line": 0, "character": 0}},
+     "newText": "x"}]}]}
+-/
+#guard_msgs in
+#eval toJson <| WorkspaceEdit.ofTextEdit { uri := "file:///a.lean" }
+  { range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, newText := "x" }
+
+/-! Deserialization accepts a missing `version`, `null` and a number. -/
+
+/-- info: [Except.ok none, Except.ok none, Except.ok (some 3)] -/
+#guard_msgs in
+#eval [r#"{"uri": "u"}"#, r#"{"uri": "u", "version": null}"#, r#"{"uri": "u", "version": 3}"#].map
+  fun s => (Json.parse s >>= fromJson? (α := VersionedTextDocumentIdentifier)).map (·.version)
+
+/-! `fromJson?` inverts `toJson`, also inside a `WorkspaceEdit`. -/
+
+/-- info: [true, true] -/
+#guard_msgs in
+#eval ([{ uri := "file:///a.lean" }, { uri := "file:///a.lean", version := some 3 }] :
+    List VersionedTextDocumentIdentifier).map fun i =>
+  match fromJson? (α := VersionedTextDocumentIdentifier) (toJson i) with
+  | .ok j => j.uri == i.uri && j.version == i.version
+  | .error _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval
+  let e := WorkspaceEdit.ofTextEdit { uri := "file:///a.lean" }
+    { range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, newText := "x" }
+  match fromJson? (α := WorkspaceEdit) (toJson e) with
+  | .ok e' => toJson e' == toJson e
+  | .error _ => false