Documentation

Lean.Data.Lsp.TextSync

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 := [anonymous] }

instance Lean.Lsp.instFromJsonDidOpenTextDocumentParams:

Lean.FromJson Lean.Lsp.DidOpenTextDocumentParams

Equations

Lean.Lsp.instFromJsonDidOpenTextDocumentParams = { fromJson? := [anonymous] }

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? := [anonymous] }

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 := [anonymous] }

instance Lean.Lsp.instFromJsonDidChangeTextDocumentParams:

Lean.FromJson Lean.Lsp.DidChangeTextDocumentParams

Equations

Lean.Lsp.instFromJsonDidChangeTextDocumentParams = { fromJson? := [anonymous] }

structure Lean.Lsp.SaveOptions:

Type

includeText : Bool

instance Lean.Lsp.instToJsonSaveOptions:

Lean.ToJson Lean.Lsp.SaveOptions

Equations

Lean.Lsp.instToJsonSaveOptions = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonSaveOptions:

Lean.FromJson Lean.Lsp.SaveOptions

Equations

Lean.Lsp.instFromJsonSaveOptions = { fromJson? := [anonymous] }

structure Lean.Lsp.DidCloseTextDocumentParams:

Type

textDocument : Lean.Lsp.TextDocumentIdentifier

instance Lean.Lsp.instToJsonDidCloseTextDocumentParams:

Lean.ToJson Lean.Lsp.DidCloseTextDocumentParams

Equations

Lean.Lsp.instToJsonDidCloseTextDocumentParams = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonDidCloseTextDocumentParams:

Lean.FromJson Lean.Lsp.DidCloseTextDocumentParams

Equations

Lean.Lsp.instFromJsonDidCloseTextDocumentParams = { fromJson? := [anonymous] }

structure Lean.Lsp.TextDocumentSyncOptions:

Type

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 := [anonymous] }

instance Lean.Lsp.instFromJsonTextDocumentSyncOptions:

Lean.FromJson Lean.Lsp.TextDocumentSyncOptions

Equations

Lean.Lsp.instFromJsonTextDocumentSyncOptions = { fromJson? := [anonymous] }