Lean.Data.Lsp.TextSync

Section "Text Document Synchronization" of the LSP spec.

source

inductive Lean.Lsp.TextDocumentSyncKind :

Type

Instances For

source

instance Lean.Lsp.instFromJsonTextDocumentSyncKind :

FromJson TextDocumentSyncKind

Equations

source

instance Lean.Lsp.instToJsonTextDocumentSyncKind :

ToJson TextDocumentSyncKind

Equations

source

structure Lean.Lsp.DidOpenTextDocumentParams :

Type

textDocument : TextDocumentItem

Instances For

source

instance Lean.Lsp.instToJsonDidOpenTextDocumentParams :

ToJson DidOpenTextDocumentParams

Equations

source

instance Lean.Lsp.instFromJsonDidOpenTextDocumentParams :

FromJson DidOpenTextDocumentParams

Equations

source

structure Lean.Lsp.TextDocumentChangeRegistrationOptions :

Type

documentSelector? : Option DocumentSelector
syncKind : TextDocumentSyncKind

Instances For

source

instance Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions :

FromJson TextDocumentChangeRegistrationOptions

Equations

source

inductive Lean.Lsp.TextDocumentContentChangeEvent :

Type

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

Instances For

source

instance Lean.Lsp.instFromJsonTextDocumentContentChangeEvent :

FromJson TextDocumentContentChangeEvent

Equations

source

instance Lean.Lsp.TextDocumentContentChangeEvent.hasToJson :

ToJson TextDocumentContentChangeEvent

Equations

source

structure Lean.Lsp.DidChangeTextDocumentParams :

Type

textDocument : VersionedTextDocumentIdentifier
contentChanges : Array TextDocumentContentChangeEvent

Instances For

source

instance Lean.Lsp.instToJsonDidChangeTextDocumentParams :

ToJson DidChangeTextDocumentParams

Equations

source

instance Lean.Lsp.instFromJsonDidChangeTextDocumentParams :

FromJson DidChangeTextDocumentParams

Equations

source

structure Lean.Lsp.DidSaveTextDocumentParams :

Type

textDocument : TextDocumentIdentifier
text? : Option String

Instances For

source

instance Lean.Lsp.instToJsonDidSaveTextDocumentParams :

ToJson DidSaveTextDocumentParams

Equations

source

instance Lean.Lsp.instFromJsonDidSaveTextDocumentParams :

FromJson DidSaveTextDocumentParams

Equations

source

structure Lean.Lsp.SaveOptions :

Type

includeText : Bool

Instances For

source

instance Lean.Lsp.instToJsonSaveOptions :

ToJson SaveOptions

Equations

source

instance Lean.Lsp.instFromJsonSaveOptions :

FromJson SaveOptions

Equations

source

structure Lean.Lsp.DidCloseTextDocumentParams :

Type

textDocument : TextDocumentIdentifier

Instances For

source

instance Lean.Lsp.instToJsonDidCloseTextDocumentParams :

ToJson DidCloseTextDocumentParams

Equations

source

instance Lean.Lsp.instFromJsonDidCloseTextDocumentParams :

FromJson DidCloseTextDocumentParams

Equations

source

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

source

instance Lean.Lsp.instToJsonTextDocumentSyncOptions :

ToJson TextDocumentSyncOptions

Equations

source

instance Lean.Lsp.instFromJsonTextDocumentSyncOptions :

FromJson TextDocumentSyncOptions

Equations