Section "Text Document Synchronization" of the LSP spec.

inductive Lean.Lsp.TextDocumentSyncKind : Type

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

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

instance Lean.Lsp.instToJsonDidOpenTextDocumentParams : ToJson DidOpenTextDocumentParams

Equations

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

def Lean.Lsp.instToJsonDidOpenTextDocumentParams.toJson : DidOpenTextDocumentParams → Json

Equations

• Lean.Lsp.instToJsonDidOpenTextDocumentParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)]].flatten

instance Lean.Lsp.instFromJsonDidOpenTextDocumentParams : FromJson DidOpenTextDocumentParams

Equations

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

def Lean.Lsp.instFromJsonDidOpenTextDocumentParams.fromJson : Json → Except String DidOpenTextDocumentParams

Equations

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

structure Lean.Lsp.TextDocumentChangeRegistrationOptions : Type

• documentSelector? : Option DocumentSelector
• syncKind : TextDocumentSyncKind

def Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions.fromJson : Json → Except String TextDocumentChangeRegistrationOptions

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions : FromJson TextDocumentChangeRegistrationOptions

Equations

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

inductive Lean.Lsp.TextDocumentContentChangeEvent : Type

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

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

instance Lean.Lsp.instToJsonDidChangeTextDocumentParams : ToJson DidChangeTextDocumentParams

Equations

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

def Lean.Lsp.instToJsonDidChangeTextDocumentParams.toJson : DidChangeTextDocumentParams → Json

Equations

• Lean.Lsp.instToJsonDidChangeTextDocumentParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("contentChanges", Lean.toJson x✝.contentChanges)]].flatten

instance Lean.Lsp.instFromJsonDidChangeTextDocumentParams : FromJson DidChangeTextDocumentParams

Equations

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

def Lean.Lsp.instFromJsonDidChangeTextDocumentParams.fromJson : Json → Except String DidChangeTextDocumentParams

Equations

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

structure Lean.Lsp.DidSaveTextDocumentParams : Type

• textDocument : TextDocumentIdentifier
• text? : Option String

instance Lean.Lsp.instToJsonDidSaveTextDocumentParams : ToJson DidSaveTextDocumentParams

Equations

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

def Lean.Lsp.instToJsonDidSaveTextDocumentParams.toJson : DidSaveTextDocumentParams → Json

Equations

• Lean.Lsp.instToJsonDidSaveTextDocumentParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], Lean.Json.opt "text" x✝.text?].flatten

instance Lean.Lsp.instFromJsonDidSaveTextDocumentParams : FromJson DidSaveTextDocumentParams

Equations

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

def Lean.Lsp.instFromJsonDidSaveTextDocumentParams.fromJson : Json → Except String DidSaveTextDocumentParams

Equations

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

structure Lean.Lsp.SaveOptions : Type

• includeText : Bool

def Lean.Lsp.instToJsonSaveOptions.toJson : SaveOptions → Json

Equations

• Lean.Lsp.instToJsonSaveOptions.toJson x✝ = Lean.Json.mkObj [[("includeText", Lean.toJson x✝.includeText)]].flatten

instance Lean.Lsp.instToJsonSaveOptions : ToJson SaveOptions

Equations

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

def Lean.Lsp.instFromJsonSaveOptions.fromJson : Json → Except String SaveOptions

Equations

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

instance Lean.Lsp.instFromJsonSaveOptions : FromJson SaveOptions

Equations

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

structure Lean.Lsp.DidCloseTextDocumentParams : Type

• textDocument : TextDocumentIdentifier

def Lean.Lsp.instToJsonDidCloseTextDocumentParams.toJson : DidCloseTextDocumentParams → Json

Equations

• Lean.Lsp.instToJsonDidCloseTextDocumentParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)]].flatten

instance Lean.Lsp.instToJsonDidCloseTextDocumentParams : ToJson DidCloseTextDocumentParams

Equations

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

instance Lean.Lsp.instFromJsonDidCloseTextDocumentParams : FromJson DidCloseTextDocumentParams

Equations

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

def Lean.Lsp.instFromJsonDidCloseTextDocumentParams.fromJson : Json → Except String DidCloseTextDocumentParams

Equations

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

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

def Lean.Lsp.instToJsonTextDocumentSyncOptions.toJson : TextDocumentSyncOptions → Json

Equations

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

instance Lean.Lsp.instToJsonTextDocumentSyncOptions : ToJson TextDocumentSyncOptions

Equations

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

def Lean.Lsp.instFromJsonTextDocumentSyncOptions.fromJson : Json → Except String TextDocumentSyncOptions

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentSyncOptions : FromJson TextDocumentSyncOptions

Equations

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