Section "Text Document Synchronization" of the LSP spec.

inductive Lean.Lsp.TextDocumentSyncKind : Type

• none : TextDocumentSyncKind
• full : TextDocumentSyncKind
• incremental : TextDocumentSyncKind

Instances For

• Lean.Lsp.instFromJsonTextDocumentSyncKind
• Lean.Lsp.instToJsonTextDocumentSyncKind

instance Lean.Lsp.instFromJsonTextDocumentSyncKind : FromJson TextDocumentSyncKind

Equations

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

instance Lean.Lsp.instToJsonTextDocumentSyncKind : ToJson TextDocumentSyncKind

Equations

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

structure Lean.Lsp.DidOpenTextDocumentParams : Type

• textDocument : TextDocumentItem

Instances For

• Lean.Lsp.instFileSourceDidOpenTextDocumentParams
• Lean.Lsp.instFromJsonDidOpenTextDocumentParams
• Lean.Lsp.instToJsonDidOpenTextDocumentParams

instance Lean.Lsp.instToJsonDidOpenTextDocumentParams : ToJson DidOpenTextDocumentParams

Equations

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

instance Lean.Lsp.instFromJsonDidOpenTextDocumentParams : FromJson DidOpenTextDocumentParams

Equations

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

structure Lean.Lsp.TextDocumentChangeRegistrationOptions : Type

• documentSelector? : Option DocumentSelector
• syncKind : TextDocumentSyncKind

Instances For

• Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions

instance Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions : FromJson TextDocumentChangeRegistrationOptions

Equations

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

inductive Lean.Lsp.TextDocumentContentChangeEvent : Type

• rangeChange (range : Range) (text : String) : TextDocumentContentChangeEvent
• fullChange (text : String) : TextDocumentContentChangeEvent

Instances For

• Lean.Lsp.TextDocumentContentChangeEvent.hasToJson
• Lean.Lsp.instFromJsonTextDocumentContentChangeEvent

instance Lean.Lsp.instFromJsonTextDocumentContentChangeEvent : FromJson TextDocumentContentChangeEvent

Equations

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

instance Lean.Lsp.TextDocumentContentChangeEvent.hasToJson : ToJson TextDocumentContentChangeEvent

Equations

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

structure Lean.Lsp.DidChangeTextDocumentParams : Type

• textDocument : VersionedTextDocumentIdentifier
• contentChanges : Array TextDocumentContentChangeEvent

Instances For

• Lean.Lsp.instFileSourceDidChangeTextDocumentParams
• Lean.Lsp.instFromJsonDidChangeTextDocumentParams
• Lean.Lsp.instToJsonDidChangeTextDocumentParams

instance Lean.Lsp.instToJsonDidChangeTextDocumentParams : ToJson DidChangeTextDocumentParams

Equations

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

instance Lean.Lsp.instFromJsonDidChangeTextDocumentParams : FromJson DidChangeTextDocumentParams

Equations

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

structure Lean.Lsp.DidSaveTextDocumentParams : Type

• textDocument : TextDocumentIdentifier
• text? : Option String

Instances For

• Lean.Lsp.instFileSourceDidSaveTextDocumentParams
• Lean.Lsp.instFromJsonDidSaveTextDocumentParams
• Lean.Lsp.instToJsonDidSaveTextDocumentParams

instance Lean.Lsp.instToJsonDidSaveTextDocumentParams : ToJson DidSaveTextDocumentParams

Equations

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

instance Lean.Lsp.instFromJsonDidSaveTextDocumentParams : FromJson DidSaveTextDocumentParams

Equations

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

structure Lean.Lsp.SaveOptions : Type

• includeText : Bool

Instances For

• Lean.Lsp.instFromJsonSaveOptions
• Lean.Lsp.instToJsonSaveOptions

instance Lean.Lsp.instToJsonSaveOptions : ToJson SaveOptions

Equations

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

instance Lean.Lsp.instFromJsonSaveOptions : FromJson SaveOptions

Equations

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

structure Lean.Lsp.DidCloseTextDocumentParams : Type

• textDocument : TextDocumentIdentifier

Instances For

• Lean.Lsp.instFileSourceDidCloseTextDocumentParams
• Lean.Lsp.instFromJsonDidCloseTextDocumentParams
• Lean.Lsp.instToJsonDidCloseTextDocumentParams

instance Lean.Lsp.instToJsonDidCloseTextDocumentParams : ToJson DidCloseTextDocumentParams

Equations

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

instance Lean.Lsp.instFromJsonDidCloseTextDocumentParams : FromJson 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 : TextDocumentSyncKind
• willSave : Bool
• willSaveWaitUntil : Bool
• save? : Option SaveOptions

Instances For

• Lean.Lsp.instFromJsonTextDocumentSyncOptions
• Lean.Lsp.instToJsonTextDocumentSyncOptions

instance Lean.Lsp.instToJsonTextDocumentSyncOptions : ToJson TextDocumentSyncOptions

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentSyncOptions : FromJson TextDocumentSyncOptions

Equations

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