Documentation

Lean.Data.Lsp.Diagnostics

Definitions and functionality for emitting diagnostic information such as errors, warnings and #command outputs from the LSP server.

inductive Lean.Lsp.DiagnosticSeverity:

Type

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

instance Lean.Lsp.instInhabitedDiagnosticSeverity:

Inhabited Lean.Lsp.DiagnosticSeverity

Equations

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

instance Lean.Lsp.instBEqDiagnosticSeverity:

BEq Lean.Lsp.DiagnosticSeverity

Equations

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

instance Lean.Lsp.instFromJsonDiagnosticSeverity:

Lean.FromJson Lean.Lsp.DiagnosticSeverity

Equations

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

instance Lean.Lsp.instToJsonDiagnosticSeverity:

Lean.ToJson Lean.Lsp.DiagnosticSeverity

Equations

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

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

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

instance Lean.Lsp.instToJsonDiagnosticCode:

Lean.ToJson Lean.Lsp.DiagnosticCode

Equations

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

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

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

instance Lean.Lsp.instToJsonDiagnosticTag:

Lean.ToJson Lean.Lsp.DiagnosticTag

Equations

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

structure Lean.Lsp.DiagnosticRelatedInformation:

Type

location : Lean.Lsp.Location
message : String

instance Lean.Lsp.instInhabitedDiagnosticRelatedInformation:

Inhabited Lean.Lsp.DiagnosticRelatedInformation

Equations

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

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] }

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

Type

range : Lean.Lsp.Range
Extension: preserve semantic range of errors when truncating them for display purposes.
fullRange : Lean.Lsp.Range
severity? : Option Lean.Lsp.DiagnosticSeverity
code? : Option Lean.Lsp.DiagnosticCode
source? : Option String
Parametrised by the type of message data. LSP diagnostics use String, whereas in Lean's interactive diagnostics we use the type of widget-enriched text. See Lean.Widget.InteractiveDiagnostic.
message : α
tags? : Option (Array Lean.Lsp.DiagnosticTag)
relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)

instance Lean.Lsp.instInhabitedDiagnosticWith:

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

Equations

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

instance Lean.Lsp.instBEqDiagnosticWith:

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

Equations

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

instance Lean.Lsp.instToJsonDiagnosticWith:

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

Equations

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

instance Lean.Lsp.instFromJsonDiagnosticWith:

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

Equations

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

@[inline]

abbrev Lean.Lsp.Diagnostic:

Type

Equations

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

structure Lean.Lsp.PublishDiagnosticsParams:

Type

instance Lean.Lsp.instInhabitedPublishDiagnosticsParams:

Inhabited Lean.Lsp.PublishDiagnosticsParams

Equations

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

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] }

instance Lean.Lsp.instFromJsonPublishDiagnosticsParams:

Lean.FromJson Lean.Lsp.PublishDiagnosticsParams

Equations

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