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

Equations

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

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

Equations

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

structure Lean.Lsp.DidOpenTextDocumentParams : Type

• textDocument : Lean.Lsp.TextDocumentItem

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

Equations

• Lean.Lsp.instToJsonDidOpenTextDocumentParams = { toJson := Lean.Lsp.toJsonDidOpenTextDocumentParams✝ }

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

Equations

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

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

Equations

• Lean.Lsp.instToJsonDidChangeTextDocumentParams = { toJson := Lean.Lsp.toJsonDidChangeTextDocumentParams✝ }

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

Equations

• Lean.Lsp.instFromJsonDidChangeTextDocumentParams = { fromJson? := Lean.Lsp.fromJsonDidChangeTextDocumentParams✝ }

structure Lean.Lsp.SaveOptions : Type

• includeText : Bool

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

Equations

• Lean.Lsp.instToJsonSaveOptions = { toJson := Lean.Lsp.toJsonSaveOptions✝ }

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

Equations

• Lean.Lsp.instFromJsonSaveOptions = { fromJson? := Lean.Lsp.fromJsonSaveOptions✝ }

structure Lean.Lsp.DidCloseTextDocumentParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

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

Equations

• Lean.Lsp.instToJsonDidCloseTextDocumentParams = { toJson := Lean.Lsp.toJsonDidCloseTextDocumentParams✝ }

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

Equations

• Lean.Lsp.instFromJsonDidCloseTextDocumentParams = { fromJson? := Lean.Lsp.fromJsonDidCloseTextDocumentParams✝ }

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

Equations

• Lean.Lsp.instFromJsonTextDocumentSyncOptions = { fromJson? := Lean.Lsp.fromJsonTextDocumentSyncOptions✝ }