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

LSP: Diagnostic; LSP: textDocument/publishDiagnostics

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 := Lean.Lsp.beqDiagnosticSeverity✝ }

instance Lean.Lsp.instOrdDiagnosticSeverity : Ord Lean.Lsp.DiagnosticSeverity

Equations

• Lean.Lsp.instOrdDiagnosticSeverity = { compare := Lean.Lsp.ordDiagnosticSeverity✝ }

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

Some languages have specific codes for each error 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 := Lean.Lsp.beqDiagnosticCode✝ }

instance Lean.Lsp.instOrdDiagnosticCode : Ord Lean.Lsp.DiagnosticCode

Equations

• Lean.Lsp.instOrdDiagnosticCode = { compare := Lean.Lsp.ordDiagnosticCode✝ }

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

Tags representing additional metadata about the diagnostic.

• unnecessary: Lean.Lsp.DiagnosticTag

  Unused or unnecessary code. Rendered as faded out eg for unused variables.

• deprecated: Lean.Lsp.DiagnosticTag

  Deprecated or obsolete code. Rendered with a strike-through.

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 := Lean.Lsp.beqDiagnosticTag✝ }

instance Lean.Lsp.instOrdDiagnosticTag : Ord Lean.Lsp.DiagnosticTag

Equations

• Lean.Lsp.instOrdDiagnosticTag = { compare := Lean.Lsp.ordDiagnosticTag✝ }

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

Represents a related message and source code location for a diagnostic. This should be used to point to code locations that cause or are related to a diagnostics, e.g when duplicating a symbol in a scope.

• 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 := Lean.Lsp.beqDiagnosticRelatedInformation✝ }

instance Lean.Lsp.instToJsonDiagnosticRelatedInformation : Lean.ToJson Lean.Lsp.DiagnosticRelatedInformation

Equations

• Lean.Lsp.instToJsonDiagnosticRelatedInformation = { toJson := Lean.Lsp.toJsonDiagnosticRelatedInformation✝ }

instance Lean.Lsp.instFromJsonDiagnosticRelatedInformation : Lean.FromJson Lean.Lsp.DiagnosticRelatedInformation

Equations

• Lean.Lsp.instFromJsonDiagnosticRelatedInformation = { fromJson? := Lean.Lsp.fromJsonDiagnosticRelatedInformation✝ }

instance Lean.Lsp.instOrdDiagnosticRelatedInformation : Ord Lean.Lsp.DiagnosticRelatedInformation

Equations

• Lean.Lsp.instOrdDiagnosticRelatedInformation = { compare := Lean.Lsp.ordDiagnosticRelatedInformation✝ }

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

Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.

LSP accepts a Diagnostic := DiagnosticWith String. The infoview also accepts InteractiveDiagnostic := DiagnosticWith (TaggedText MsgEmbed).

reference

• range : Lean.Lsp.Range

  The range at which the message applies.

• fullRange? : Option Lean.Lsp.Range

  Extension: preserve semantic range of errors when truncating them for display purposes.

• severity? : Option Lean.Lsp.DiagnosticSeverity
• code? : Option Lean.Lsp.DiagnosticCode

  The diagnostic's code, which might appear in the user interface.

• source? : Option String

  A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'.

• message : α

  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.

• tags? : Option (Array Lean.Lsp.DiagnosticTag)

  Additional metadata about the diagnostic.

• relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)

  An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property.

• data? : Option Lean.Json

  A data entry field that is preserved between a textDocument/publishDiagnostics notification and textDocument/codeAction request.

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 := Lean.Lsp.beqDiagnosticWith✝ }

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

Equations

• Lean.Lsp.instToJsonDiagnosticWith = { toJson := Lean.Lsp.toJsonDiagnosticWith✝ }

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

Equations

• Lean.Lsp.instFromJsonDiagnosticWith = { fromJson? := Lean.Lsp.fromJsonDiagnosticWith✝ }

def Lean.Lsp.DiagnosticWith.fullRange {α : Type} (d : Lean.Lsp.DiagnosticWith α) : Lean.Lsp.Range

Equations

• d.fullRange = d.fullRange?.getD d.range

def Lean.Lsp.instOrdArray_lean {α : Type u_1} [Ord α] : Ord (Array α)

Equations

• Lean.Lsp.instOrdArray_lean = Ord.arrayOrd

instance Lean.Lsp.DiagnosticWith.instOrdUserVisible : {α : Type} → [inst : Ord α] → Ord (Lean.Lsp.DiagnosticWith.UserVisible α)

Equations

• Lean.Lsp.DiagnosticWith.instOrdUserVisible = { compare := Lean.Lsp.DiagnosticWith.ordUserVisible✝ }

def Lean.Lsp.compareByUserVisible {α : Type} [Ord α] (a : Lean.Lsp.DiagnosticWith α) (b : Lean.Lsp.DiagnosticWith α) : Ordering

Compares DiagnosticWith instances modulo non-user-facing properties.

Equations

• Lean.Lsp.compareByUserVisible a b = compare (Lean.Lsp.DiagnosticWith.UserVisible.ofDiagnostic a) (Lean.Lsp.DiagnosticWith.UserVisible.ofDiagnostic b)

@[reducible, inline]

abbrev Lean.Lsp.Diagnostic : Type

Equations

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

structure Lean.Lsp.PublishDiagnosticsParams : Type

Parameters for the textDocument/publishDiagnostics notification.

• 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.instBEqPublishDiagnosticsParams : BEq Lean.Lsp.PublishDiagnosticsParams

Equations

• Lean.Lsp.instBEqPublishDiagnosticsParams = { beq := Lean.Lsp.beqPublishDiagnosticsParams✝ }

instance Lean.Lsp.instToJsonPublishDiagnosticsParams : Lean.ToJson Lean.Lsp.PublishDiagnosticsParams

Equations

• Lean.Lsp.instToJsonPublishDiagnosticsParams = { toJson := Lean.Lsp.toJsonPublishDiagnosticsParams✝ }

instance Lean.Lsp.instFromJsonPublishDiagnosticsParams : Lean.FromJson Lean.Lsp.PublishDiagnosticsParams

Equations

• Lean.Lsp.instFromJsonPublishDiagnosticsParams = { fromJson? := Lean.Lsp.fromJsonPublishDiagnosticsParams✝ }