Section "Text Document Synchronization" of the LSP spec.
- none : TextDocumentSyncKind
- full : TextDocumentSyncKind
- incremental : TextDocumentSyncKind
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- documentSelector? : Option DocumentSelector
- syncKind : TextDocumentSyncKind
- rangeChange (range : Range) (text : String) : TextDocumentContentChangeEvent
- fullChange (text : String) : TextDocumentContentChangeEvent
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- textDocument : VersionedTextDocumentIdentifier
- contentChanges : Array TextDocumentContentChangeEvent
- includeText : Bool
Equations
- Lean.Lsp.instToJsonSaveOptions = { toJson := Lean.Lsp.toJsonSaveOptions✝ }
Equations
- Lean.Lsp.instFromJsonSaveOptions = { fromJson? := Lean.Lsp.fromJsonSaveOptions✝ }
NOTE: This is defined twice in the spec. The latter version has more fields.
- openClose : Bool
- change : TextDocumentSyncKind
- willSave : Bool
- willSaveWaitUntil : Bool
- save? : Option SaveOptions