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

Equations

• Lean.Lsp.instFromJsonDidOpenTextDocumentParams = { fromJson? := Lean.Lsp.fromJsonDidOpenTextDocumentParams✝ }

structure Lean.Lsp.TextDocumentChangeRegistrationOptions : Type

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

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

Equations

• Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions = { fromJson? := Lean.Lsp.fromJsonTextDocumentChangeRegistrationOptions✝ }

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

Equations

• One or more equations did not get rendered due to their size.

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.DidSaveTextDocumentParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier
• text? : Option String

instance Lean.Lsp.instToJsonDidSaveTextDocumentParams : Lean.ToJson Lean.Lsp.DidSaveTextDocumentParams

Equations

• Lean.Lsp.instToJsonDidSaveTextDocumentParams = { toJson := Lean.Lsp.toJsonDidSaveTextDocumentParams✝ }

instance Lean.Lsp.instFromJsonDidSaveTextDocumentParams : Lean.FromJson Lean.Lsp.DidSaveTextDocumentParams

Equations

• Lean.Lsp.instFromJsonDidSaveTextDocumentParams = { fromJson? := Lean.Lsp.fromJsonDidSaveTextDocumentParams✝ }

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

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

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

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

Equations

• Lean.Lsp.instToJsonTextDocumentSyncOptions = { toJson := Lean.Lsp.toJsonTextDocumentSyncOptions✝ }

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