Section "Text Document Synchronization" of the LSP spec.

inductive Lean.Lsp.TextDocumentSyncKind : Type

• none: Lean.Lsp.TextDocumentSyncKind
• full: Lean.Lsp.TextDocumentSyncKind
• incremental: Lean.Lsp.TextDocumentSyncKind

instance Lean.Lsp.instFromJsonTextDocumentSyncKind : Lean.FromJson Lean.Lsp.TextDocumentSyncKind

instance Lean.Lsp.instToJsonTextDocumentSyncKind : Lean.ToJson Lean.Lsp.TextDocumentSyncKind

structure Lean.Lsp.DidOpenTextDocumentParams : Type

• textDocument : Lean.Lsp.TextDocumentItem

instance Lean.Lsp.instToJsonDidOpenTextDocumentParams : Lean.ToJson Lean.Lsp.DidOpenTextDocumentParams

instance Lean.Lsp.instFromJsonDidOpenTextDocumentParams : Lean.FromJson Lean.Lsp.DidOpenTextDocumentParams

structure Lean.Lsp.TextDocumentChangeRegistrationOptions : Type

• documentSelector? : Option Lean.Lsp.DocumentSelector
• syncKind : Lean.Lsp.TextDocumentSyncKind

instance Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions : Lean.FromJson Lean.Lsp.TextDocumentChangeRegistrationOptions

inductive Lean.Lsp.TextDocumentContentChangeEvent : Type

• rangeChange: Lean.Lsp.Range → String → Lean.Lsp.TextDocumentContentChangeEvent
• fullChange: String → Lean.Lsp.TextDocumentContentChangeEvent

instance Lean.Lsp.instFromJsonTextDocumentContentChangeEvent : Lean.FromJson Lean.Lsp.TextDocumentContentChangeEvent

instance Lean.Lsp.TextDocumentContentChangeEvent.hasToJson : Lean.ToJson Lean.Lsp.TextDocumentContentChangeEvent

structure Lean.Lsp.DidChangeTextDocumentParams : Type

• textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
• contentChanges : Array Lean.Lsp.TextDocumentContentChangeEvent

instance Lean.Lsp.instToJsonDidChangeTextDocumentParams : Lean.ToJson Lean.Lsp.DidChangeTextDocumentParams

instance Lean.Lsp.instFromJsonDidChangeTextDocumentParams : Lean.FromJson Lean.Lsp.DidChangeTextDocumentParams

structure Lean.Lsp.SaveOptions : Type

• includeText : Bool

instance Lean.Lsp.instToJsonSaveOptions : Lean.ToJson Lean.Lsp.SaveOptions

instance Lean.Lsp.instFromJsonSaveOptions : Lean.FromJson Lean.Lsp.SaveOptions

structure Lean.Lsp.DidCloseTextDocumentParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

instance Lean.Lsp.instToJsonDidCloseTextDocumentParams : Lean.ToJson Lean.Lsp.DidCloseTextDocumentParams

instance Lean.Lsp.instFromJsonDidCloseTextDocumentParams : Lean.FromJson Lean.Lsp.DidCloseTextDocumentParams

structure Lean.Lsp.TextDocumentSyncOptions : Type

• openClose : Bool
• change : Lean.Lsp.TextDocumentSyncKind
• willSave : Bool
• willSaveWaitUntil : Bool
• save? : Option Lean.Lsp.SaveOptions

NOTE: This is defined twice in the spec. The latter version has more fields.

instance Lean.Lsp.instToJsonTextDocumentSyncOptions : Lean.ToJson Lean.Lsp.TextDocumentSyncOptions

instance Lean.Lsp.instFromJsonTextDocumentSyncOptions : Lean.FromJson Lean.Lsp.TextDocumentSyncOptions