Documentation

Lean.Data.Lsp.TextSync

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

Lean.Lsp.instFromJsonTextDocumentSyncKind = { fromJson? := fun j => match Lean.Json.getNat? j with | Except.ok 0 => pure Lean.Lsp.TextDocumentSyncKind.none | Except.ok 1 => pure Lean.Lsp.TextDocumentSyncKind.full | Except.ok 2 => pure Lean.Lsp.TextDocumentSyncKind.incremental | x => throw "unknown TextDocumentSyncKind" }

instance Lean.Lsp.instToJsonTextDocumentSyncKind :

Lean.ToJson Lean.Lsp.TextDocumentSyncKind

Equations

Lean.Lsp.instToJsonTextDocumentSyncKind = { toJson := fun x => match x with | Lean.Lsp.TextDocumentSyncKind.none => 0 | Lean.Lsp.TextDocumentSyncKind.full => 1 | Lean.Lsp.TextDocumentSyncKind.incremental => 2 }

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

Lean.Lsp.instFromJsonTextDocumentContentChangeEvent = { fromJson? := fun j => HOrElse.hOrElse (do let range ← Lean.Json.getObjValAs? j Lean.Lsp.Range "range" let text ← Lean.Json.getObjValAs? j String "text" pure (Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range text)) fun x => Lean.Lsp.TextDocumentContentChangeEvent.fullChange <$> Lean.Json.getObjValAs? j String "text" }

instance Lean.Lsp.TextDocumentContentChangeEvent.hasToJson :

Lean.ToJson Lean.Lsp.TextDocumentContentChangeEvent

Equations

Lean.Lsp.TextDocumentContentChangeEvent.hasToJson = { toJson := fun o => Lean.Json.mkObj (match o with | Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range text => [("range", Lean.toJson range), ("text", Lean.toJson text)] | Lean.Lsp.TextDocumentContentChangeEvent.fullChange text => [("text", Lean.toJson text)]) }

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.instFromJsonSaveOptions :

Lean.FromJson Lean.Lsp.SaveOptions

Equations

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

instance Lean.Lsp.instToJsonSaveOptions :

Lean.ToJson Lean.Lsp.SaveOptions

Equations

Lean.Lsp.instToJsonSaveOptions = { toJson := [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] }