Documentation

Lean.Data.Lsp.Diagnostics

inductive Lean.Lsp.DiagnosticSeverity :

Type

error: Lean.Lsp.DiagnosticSeverity
warning: Lean.Lsp.DiagnosticSeverity
information: Lean.Lsp.DiagnosticSeverity
hint: Lean.Lsp.DiagnosticSeverity

instance Lean.Lsp.instBEqDiagnosticSeverity :

BEq Lean.Lsp.DiagnosticSeverity

Equations

Lean.Lsp.instBEqDiagnosticSeverity = { beq := [anonymous] }

instance Lean.Lsp.instInhabitedDiagnosticSeverity :

Inhabited Lean.Lsp.DiagnosticSeverity

Equations

Lean.Lsp.instInhabitedDiagnosticSeverity = { default := Lean.Lsp.DiagnosticSeverity.error }

instance Lean.Lsp.instFromJsonDiagnosticSeverity :

Lean.FromJson Lean.Lsp.DiagnosticSeverity

Equations

Lean.Lsp.instFromJsonDiagnosticSeverity = { fromJson? := fun j => match Lean.Json.getNat? j with | Except.ok 1 => pure Lean.Lsp.DiagnosticSeverity.error | Except.ok 2 => pure Lean.Lsp.DiagnosticSeverity.warning | Except.ok 3 => pure Lean.Lsp.DiagnosticSeverity.information | Except.ok 4 => pure Lean.Lsp.DiagnosticSeverity.hint | x => throw (toString "unknown DiagnosticSeverity '" ++ toString j ++ toString "'") }

instance Lean.Lsp.instToJsonDiagnosticSeverity :

Lean.ToJson Lean.Lsp.DiagnosticSeverity

Equations

Lean.Lsp.instToJsonDiagnosticSeverity = { toJson := fun x => match x with | Lean.Lsp.DiagnosticSeverity.error => 1 | Lean.Lsp.DiagnosticSeverity.warning => 2 | Lean.Lsp.DiagnosticSeverity.information => 3 | Lean.Lsp.DiagnosticSeverity.hint => 4 }

inductive Lean.Lsp.DiagnosticCode :

Type

int: Int → Lean.Lsp.DiagnosticCode
string: String → Lean.Lsp.DiagnosticCode

instance Lean.Lsp.instInhabitedDiagnosticCode :

Inhabited Lean.Lsp.DiagnosticCode

Equations

Lean.Lsp.instInhabitedDiagnosticCode = { default := Lean.Lsp.DiagnosticCode.int default }

instance Lean.Lsp.instBEqDiagnosticCode :

BEq Lean.Lsp.DiagnosticCode

Equations

Lean.Lsp.instBEqDiagnosticCode = { beq := [anonymous] }

instance Lean.Lsp.instFromJsonDiagnosticCode :

Lean.FromJson Lean.Lsp.DiagnosticCode

Equations

Lean.Lsp.instFromJsonDiagnosticCode = { fromJson? := fun x => match x with | Lean.Json.num { mantissa := i, exponent := 0 } => pure (Lean.Lsp.DiagnosticCode.int i) | Lean.Json.str s => pure (Lean.Lsp.DiagnosticCode.string s) | j => throw (toString "expected string or integer diagnostic code, got '" ++ toString j ++ toString "'") }

instance Lean.Lsp.instToJsonDiagnosticCode :

Lean.ToJson Lean.Lsp.DiagnosticCode

Equations

Lean.Lsp.instToJsonDiagnosticCode = { toJson := fun x => match x with | Lean.Lsp.DiagnosticCode.int i => Lean.Json.num (Lean.JsonNumber.fromInt i) | Lean.Lsp.DiagnosticCode.string s => Lean.Json.str s }

inductive Lean.Lsp.DiagnosticTag :

Type

unnecessary: Lean.Lsp.DiagnosticTag
deprecated: Lean.Lsp.DiagnosticTag

instance Lean.Lsp.instInhabitedDiagnosticTag :

Inhabited Lean.Lsp.DiagnosticTag

Equations

Lean.Lsp.instInhabitedDiagnosticTag = { default := Lean.Lsp.DiagnosticTag.unnecessary }

instance Lean.Lsp.instBEqDiagnosticTag :

BEq Lean.Lsp.DiagnosticTag

Equations

Lean.Lsp.instBEqDiagnosticTag = { beq := [anonymous] }

instance Lean.Lsp.instFromJsonDiagnosticTag :

Lean.FromJson Lean.Lsp.DiagnosticTag

Equations

Lean.Lsp.instFromJsonDiagnosticTag = { fromJson? := fun j => match Lean.Json.getNat? j with | Except.ok 1 => pure Lean.Lsp.DiagnosticTag.unnecessary | Except.ok 2 => pure Lean.Lsp.DiagnosticTag.deprecated | x => throw "unknown DiagnosticTag" }

instance Lean.Lsp.instToJsonDiagnosticTag :

Lean.ToJson Lean.Lsp.DiagnosticTag

Equations

Lean.Lsp.instToJsonDiagnosticTag = { toJson := fun x => match x with | Lean.Lsp.DiagnosticTag.unnecessary => Lean.Json.num (Lean.JsonNumber.fromNat 1) | Lean.Lsp.DiagnosticTag.deprecated => Lean.Json.num (Lean.JsonNumber.fromNat 2) }

structure Lean.Lsp.DiagnosticRelatedInformation :

Type

location : Lean.Lsp.Location
message : String

instance Lean.Lsp.instBEqDiagnosticRelatedInformation :

BEq Lean.Lsp.DiagnosticRelatedInformation

Equations

Lean.Lsp.instBEqDiagnosticRelatedInformation = { beq := [anonymous] }

instance Lean.Lsp.instToJsonDiagnosticRelatedInformation :

Lean.ToJson Lean.Lsp.DiagnosticRelatedInformation

Equations

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

instance Lean.Lsp.instFromJsonDiagnosticRelatedInformation :

Lean.FromJson Lean.Lsp.DiagnosticRelatedInformation

Equations

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

instance Lean.Lsp.instInhabitedDiagnosticRelatedInformation :

Inhabited Lean.Lsp.DiagnosticRelatedInformation

Equations

Lean.Lsp.instInhabitedDiagnosticRelatedInformation = { default := { location := default, message := default } }

structure Lean.Lsp.DiagnosticWith (α : Type) :

Type

range : Lean.Lsp.Range
fullRange : Lean.Lsp.Range
severity? : Option Lean.Lsp.DiagnosticSeverity
code? : Option Lean.Lsp.DiagnosticCode
source? : Option String
message : α
tags? : Option (Array Lean.Lsp.DiagnosticTag)
relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)

instance Lean.Lsp.instToJsonDiagnosticWith :

{α : Type} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Lsp.DiagnosticWith α)

Equations

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

instance Lean.Lsp.instBEqDiagnosticWith :

{α : Type} → [inst : BEq α] → BEq (Lean.Lsp.DiagnosticWith α)

Equations

Lean.Lsp.instBEqDiagnosticWith = { beq := [anonymous] }

instance Lean.Lsp.instFromJsonDiagnosticWith :

{α : Type} → [inst : Lean.FromJson α] → Lean.FromJson (Lean.Lsp.DiagnosticWith α)

Equations

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

instance Lean.Lsp.instInhabitedDiagnosticWith :

{a : Type} → [inst : Inhabited a] → Inhabited (Lean.Lsp.DiagnosticWith a)

Equations

Lean.Lsp.instInhabitedDiagnosticWith = { default := { range := default, fullRange := default, severity? := default, code? := default, source? := default, message := default, tags? := default, relatedInformation? := default } }

@[inline]

abbrev Lean.Lsp.Diagnostic :

Type

Equations

Lean.Lsp.Diagnostic = Lean.Lsp.DiagnosticWith String

structure Lean.Lsp.PublishDiagnosticsParams :

Type

uri : Lean.Lsp.DocumentUri
version? : Option Int
diagnostics : Array Lean.Lsp.Diagnostic

instance Lean.Lsp.instInhabitedPublishDiagnosticsParams :

Inhabited Lean.Lsp.PublishDiagnosticsParams

Equations

Lean.Lsp.instInhabitedPublishDiagnosticsParams = { default := { uri := default, version? := default, diagnostics := default } }

instance Lean.Lsp.instFromJsonPublishDiagnosticsParams :

Lean.FromJson Lean.Lsp.PublishDiagnosticsParams

Equations

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

instance Lean.Lsp.instBEqPublishDiagnosticsParams :

BEq Lean.Lsp.PublishDiagnosticsParams

Equations

Lean.Lsp.instBEqPublishDiagnosticsParams = { beq := [anonymous] }

instance Lean.Lsp.instToJsonPublishDiagnosticsParams :

Lean.ToJson Lean.Lsp.PublishDiagnosticsParams

Equations

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